let X be set ; :: thesis:
assume that
A1: X <> {} and
A2: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
meet Z in X ; :: thesis:
for Z being set st Z c= X & Z is c=-linear holds
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) )

set x = the Element of X;
let Z be set ; :: thesis:
assume that
A3: Z c= X and
A4: Z is c=-linear ; :: thesis:
( Z <> {} or Z = {} ) ;
then consider Y being set such that
A5: ( ( Y = meet Z & Z <> {} ) or ( Y = the Element of X & Z = {} ) ) ;
take Y ; :: thesis:
thus ( Y in X & ( for X1 being set st X1 in Z holds
Y c= X1 ) ) by A1, A2, A3, A4, A5, SETFAM_1:3; :: thesis:

end;

hence ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Z c= Y ) ) by A1, Th66; :: thesis: