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

consider Y being Element of X;
for X1 being set st X1 in Z holds
X1 c= Y by A3;
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 A1, A2; :: 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 A1, ORDERS_1:175; :: thesis: verum