defpred S₁[ 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₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) )

S₁[ card {(Bottom L),x}] by A1;
then A2: ex k being Nat st S₁[k] ;
A3: for k being Nat st S₁[k] holds
k <= card the carrier of L by NAT_1:43;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[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:
thus ( S₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) ) by A4; :: thesis:

end;

then consider k being Element of NAT such that
A5: ( S₁[k] & ( for n being Element of NAT st S₁[n] holds
n <= k ) ) ;
take k ; :: thesis:
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: