let X be set ; :: thesis: ( X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X ) 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
union Z in X ; :: 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 ) )
consider x being Element of X;
( Z <> {} or Z = {} ) ;
then consider Y being set such that
A4: ( ( Y = union Z & Z <> {} ) or ( Y = x & Z = {} ) ) ;
take Y ; :: thesis: ( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
thus ( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A1, A2, A3, A4, ZFMISC_1:92; :: thesis: verum

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