let X be non empty finite-character set ; :: thesis: ex Y being Element of X st
for Z being Element of X holds not Y c< Z
for C being set st C c= X & C is c=-linear holds
ex Y being set st
( Y in X & ( for Z being set st Z in C holds
Z c= Y ) )

proof

let C be set ; :: thesis: ( C c= X & C is c=-linear implies ex Y being set st
( Y in X & ( for Z being set st Z in C holds
Z c= Y ) ) )
assume A2: ( C c= X & C is c=-linear ) ; :: thesis: ex Y being set st
( Y in X & ( for Z being set st Z in C holds
Z c= Y ) )
take Y = union C; :: thesis: ( Y in X & ( for Z being set st Z in C holds
Z c= Y ) )
thus ( Y in X & ( for Z being set st Z in C holds
Z c= Y ) ) by A2, Lm59, ZFMISC_1:74; :: thesis: verum

end;

then consider Y being set such that
A5: Y in X and
A6: for Z being set st Z in X & Z <> Y holds
not Y c= Z by ORDERS_1:65;
reconsider Y = Y as Element of X by A5;
take Y ; :: thesis: for Z being Element of X holds not Y c< Z
let Z be Element of X; :: thesis: not Y c< Z
assume Y c< Z ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum