∀ {J : Type u_1} [inst : PartialOrder J] {α : Type u_2} [inst_1 : PartialOrder α]
  (f : PrincipalSeg (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2), Monotone ⇑(Set.principalSegIio f.top).toRelEmbedding