defpred S₁[ Nat] means ex x being Element of L st
( x in A & $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
x in A 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;

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

proof

consider x being object such that
A4: x in A 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₁[k] by A4; :: thesis: verum

end;

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

end;

then consider k being Element of NAT such that
A7: ( S₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) ) ;
consider x being Element of L such that
A8: x in A and
A9: ( k = height x & ( for n being Element of NAT st ex z being Element of L st
( z in A & n = height z ) holds
n <= k ) ) by A7;
take x ; :: thesis: ( ( for x being Element of L st x in A holds
x <= x ) & x in A )
thus for w being Element of L st w in A holds
w <= x :: thesis: x in A

proof

let w be Element of L; :: thesis: ( w in A implies w <= x )
assume A10: w in A ; :: thesis: w <= x
then height w <= height x by A9;
hence w <= x by A8, A10, Th5; :: thesis: verum

end;

thus x in A by A8; :: thesis: verum