let L be finite LATTICE; :: thesis: for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )

let X be non empty Subset of L; :: thesis: ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )

defpred S1[ Nat] means ex x being Element of L st
( x in X & \$1 = height x );
ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )
proof
A1: for k being Nat st S1[k] holds
k <= card the carrier of L
proof
let k be Nat; :: thesis: ( S1[k] implies k <= card the carrier of L )
assume S1[k] ; :: thesis: k <= card the carrier of L
then consider x being Element of L such that
x in X and
A2: k = height x ;
ex B being Chain of Bottom L,x st k = card B by ;
hence k <= card the carrier of L by NAT_1:43; :: thesis: verum
end;
A3: ex k being Nat st S1[k]
proof
consider x being object such that
A4: x in X by XBOOLE_0:def 1;
reconsider x = x as Element of L by A4;
ex B being Chain of Bottom L,x st height x = card B by Def3;
hence ex k being Nat st S1[k] by A4; :: thesis: verum
end;
consider k being Nat such that
A5: S1[k] and
A6: for n being Nat st S1[n] holds
n <= k from NAT_1:sch 6(A1, A3);
for n being Element of NAT st S1[n] holds
n <= k by A6;
hence ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) by A5; :: thesis: verum
end;
then consider k being Element of NAT such that
A7: ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) ;
consider x being Element of L such that
A8: x in X and
A9: ( k = height x & ( for n being Element of NAT st ex y being Element of L st
( y in X & n = height y ) holds
n <= k ) ) by A7;
for y being Element of L st y in X holds
not x < y
proof
let y be Element of L; :: thesis: ( y in X implies not x < y )
assume that
A10: y in X and
A11: x < y ; :: thesis: contradiction
height x < height y by ;
hence contradiction by A9, A10; :: thesis: verum
end;
hence ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) by A8; :: thesis: verum