let Y be Subset of X; :: thesis: Y is c=-linear
let x be set ; :: according to ORDINAL1:def 9 :: thesis: for b₁ being set holds
( not x in Y or not b₁ in Y or x,b₁ are_c=-comparable )
let y be set ; :: thesis: ( not x in Y or not y in Y or x,y are_c=-comparable )
assume ( x in Y & y in Y ) ; :: thesis: x,y are_c=-comparable
hence x,y are_c=-comparable by ORDINAL1:def 9; :: thesis: verum