let X be set ; :: thesis: ( X is empty implies X is c=-linear )
assume A1: X is empty ; :: thesis: X is c=-linear
let x be set ; :: according to ORDINAL1:def 8 :: thesis: for y being set st x in X & y in X holds
x,y are_c=-comparable
thus for y being set st x in X & y in X holds
x,y are_c=-comparable by A1; :: thesis: verum