let X be set ; :: thesis: ( X <> {} & ( 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 ) ) ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) )

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

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

assume A3: ( Z c= X & Z is c=-linear ) ; :: thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

per cases ( Z = {} or Z <> {} ) ;
suppose A4: Z = {} ; :: thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

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

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: verum
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 ; :: thesis: verum