let Y be Subset of X; :: thesis: Y is c=-linear
let x, y be set ; :: according to ORDINAL1:def 8 :: thesis: ( x in Y & y in Y implies 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 Def8; :: thesis: verum