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