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