set a = the Element of A;
reconsider B = { the Element of A} as non empty Subset of A ;
take B ; :: thesis: ( B is c=-linear & not B is empty )
B is c=-linear
proof
let x, y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not x in B or not y in B or x,y are_c=-comparable )
assume that
A1: x in B and
A2: y in B ; :: thesis: x,y are_c=-comparable
x = the Element of A by A1, TARSKI:def 1;
hence x,y are_c=-comparable by A2, TARSKI:def 1; :: thesis: verum
end;
hence ( B is c=-linear & not B is empty ) ; :: thesis: verum