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 S₁[ Nat] means ex x being Element of L st
( x in X & $1 = height x );
ex k being Element of NAT st
( S₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) )

proof

A1: for k being Nat st S₁[k] holds
k <= card the carrier of L

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= card the carrier of L )
assume S₁[k] ; :: thesis: k <= card the carrier of L
then consider x being Element of L such that
A2: ( x in X & k = height x ) ;
consider B being Chain of Bottom L,x such that
A3: k = card B by A2, Def3;
thus k <= card the carrier of L by A3, NAT_1:44; :: thesis: verum

end;

A4: ex k being Nat st S₁[k]

proof

consider x being set such that
A5: x in X by XBOOLE_0:def 1;
reconsider x = x as Element of L by A5;
( ex B being Chain of Bottom L,x st height x = card B & ( for B being Chain of Bottom L,x holds card B <= height x ) ) by Def3;
then consider B being Chain of Bottom L,x such that
A6: ( height x = card B & ( for B being Chain of Bottom L,x holds card B <= height x ) ) ;
thus ex k being Nat st S₁[k] by A5, A6; :: thesis: verum

end;

consider k being Nat such that
A7: S₁[k] and
A8: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A1, A4);
for n being Element of NAT st S₁[n] holds
n <= k by A8;
hence ex k being Element of NAT st
( S₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) ) by A7; :: thesis: verum

end;

then consider k being Element of NAT such that
A9: ( S₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) ) ;
consider x being Element of L such that
A10: ( x in X & 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 A9;
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 A11: ( y in X & x < y ) ; :: thesis: contradiction
then height x < height y by Th2;
hence contradiction by A10, A11; :: 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 A10; :: thesis: verum