defpred S_{1}[ Nat] means ex A being Chain of Bottom L,x st $1 = card A;

A1: {(Bottom L),x} is Chain of Bottom L,x by Th1, YELLOW_0:44;

ex k being Element of NAT st

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

n <= k ) )

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

n <= k ) ) ;

take k ; :: thesis: ( ex A being Chain of Bottom L,x st k = card A & ( for A being Chain of Bottom L,x holds card A <= k ) )

thus ( ex A being Chain of Bottom L,x st k = card A & ( for A being Chain of Bottom L,x holds card A <= k ) ) by A5; :: thesis: verum

A1: {(Bottom L),x} is Chain of Bottom L,x by Th1, YELLOW_0:44;

ex k being Element of NAT st

( S

n <= k ) )

proof

then consider k being Element of NAT such that
S_{1}[ card {(Bottom L),x}]
by A1;

then A2: ex k being Nat st S_{1}[k]
;

A3: for k being Nat st S_{1}[k] holds

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

consider k being Nat such that

A4: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

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

reconsider k = k as Element of NAT by ORDINAL1:def 12;

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

n <= k ) )

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

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

end;then A2: ex k being Nat st S

A3: for k being Nat st S

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

consider k being Nat such that

A4: ( S

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

reconsider k = k as Element of NAT by ORDINAL1:def 12;

take k ; :: thesis: ( S

n <= k ) )

thus ( S

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

A5: ( S

n <= k ) ) ;

take k ; :: thesis: ( ex A being Chain of Bottom L,x st k = card A & ( for A being Chain of Bottom L,x holds card A <= k ) )

thus ( ex A being Chain of Bottom L,x st k = card A & ( for A being Chain of Bottom L,x holds card A <= k ) ) by A5; :: thesis: verum