∀ {α : Type u_1} {β : Type u_2} {a b : α} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  (f : PrincipalSeg (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2), f.toRelEmbedding a ⩿ f.toRelEmbedding b ↔ a ⩿ b