let X be set ; :: thesis: ( X is natural-membered implies X is c=-linear )
assume A1: for x being object st x in X holds
x is natural ; :: according to MEMBERED:def 6 :: thesis: X is c=-linear
let x, y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not x in X or not y in X or x,y are_c=-comparable )
assume ( x in X & y in X ) ; :: thesis: x,y are_c=-comparable
then reconsider a = x, b = y as Nat by A1;
a,b are_c=-comparable by ORDINAL1:15;
hence x,y are_c=-comparable ; :: thesis: verum