let k, n be natural number ; :: 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:7;
hence Seg k, Seg n are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum