consider a being Element of A;
reconsider B = {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 9 :: thesis: ( not x in B or not y in B or not R5(x,y) )
assume that
A1: x in B and
A2: y in B ; :: thesis: R5(x,y)
x = a by A1, TARSKI:def 1;
hence R5(x,y) by A2, TARSKI:def 1; :: thesis: verum
end;
hence ( B is c=-linear & not B is empty ) ; :: thesis: verum