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_{1}[ Nat] means ex x being Element of L st

( x in X & $1 = height x );

ex k being Element of NAT st

( S_{1}[k] & ( for n being Element of NAT st S_{1}[n] holds

n <= k ) )

A7: ( S_{1}[k] & ( for n being Element of NAT st S_{1}[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

( x in X & ( for y being Element of L st y in X holds

not x < y ) ) by A8; :: thesis: verum

( 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

( x in X & $1 = height x );

ex k being Element of NAT st

( S

n <= k ) )

proof

then consider k being Element of NAT such that
A1:
for k being Nat st S_{1}[k] holds

k <= card the carrier of L_{1}[k]

A5: S_{1}[k]
and

A6: for n being Nat st S_{1}[n] holds

n <= k from NAT_1:sch 6(A1, A3);

for n being Element of NAT st S_{1}[n] holds

n <= k by A6;

hence ex k being Element of NAT st

( S_{1}[k] & ( for n being Element of NAT st S_{1}[n] holds

n <= k ) ) by A5; :: thesis: verum

end;k <= card the carrier of L

proof

A3:
ex k being Nat st S
let k be Nat; :: thesis: ( S_{1}[k] implies k <= card the carrier of L )

assume S_{1}[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 A2, Def3;

hence k <= card the carrier of L by NAT_1:43; :: thesis: verum

end;assume S

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 A2, Def3;

hence k <= card the carrier of L by NAT_1:43; :: thesis: verum

proof

consider k being Nat such that
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 S_{1}[k]
by A4; :: thesis: verum

end;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 S

A5: S

A6: for n being Nat st S

n <= k from NAT_1:sch 6(A1, A3);

for n being Element of NAT st S

n <= k by A6;

hence ex k being Element of NAT st

( S

n <= k ) ) by A5; :: thesis: verum

A7: ( S

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

hence
ex x being Element of L st
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 A11, Th2;

hence contradiction by A9, A10; :: thesis: verum

end;assume that

A10: y in X and

A11: x < y ; :: thesis: contradiction

height x < height y by A11, Th2;

hence contradiction by A9, A10; :: thesis: verum

( x in X & ( for y being Element of L st y in X holds

not x < y ) ) by A8; :: thesis: verum