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 9 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or x,b₁ are_c=-comparable )
let y be set ; :: thesis: ( not x in X or not y in X or x,y are_c=-comparable )
thus ( not x in X or not y in X or x,y are_c=-comparable ) by A1; :: thesis: verum