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 ) )

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Y c= Z ) ) by A1, ORDERS_1:65; :: thesis: verum

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

hence
ex Y being set st
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 ) )

end;( 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 <> {} )
;

end;

suppose A4:
Z = {}
; :: thesis: ex Y being set st

( Y in X & ( for X1 being set st X1 in Z holds

X1 c= Y ) )

( 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;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

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Y c= Z ) ) by A1, ORDERS_1:65; :: thesis: verum