let k, n be Nat; :: thesis: Seg k, Seg n are_c=-comparable
( n <= k or k <= n ) ;
then ( Seg n c= Seg k or Seg k c= Seg n ) by FINSEQ_1:5;
hence Seg k, Seg n are_c=-comparable ; :: thesis: verum