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

set x = the Element of X;
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 that
A3: Z c= X and
A4: 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 ) )
( Z <> {} or Z = {} ) ;
then consider Y being set such that
A5: ( ( Y = union Z & Z <> {} ) or ( Y = the Element of 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, A5, ZFMISC_1:74; :: 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, Th65; :: thesis: verum