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
ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) ; :: 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
X1 c= Y ) )

proof

let Z be set ; :: thesis:
assume A3: ( Z c= X & Z is c=-linear ) ; :: thesis:

per cases ;

suppose A4: Z = {} ; :: thesis:

set Y = the Element of X;
for X1 being set st X1 in Z holds
X1 c= the Element of X by A4;
hence ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A1; :: thesis:

end;

suppose Z <> {} ; :: thesis:

hence ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A2, A3; :: thesis:

end;

end;

end;

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