defpred S1[ Nat] means ex A being Chain of Bottom L,x st \$1 = card A;
A1: {(),x} is Chain of Bottom L,x by ;
ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )
proof
S1[ card {(),x}] by A1;
then A2: ex k being Nat st S1[k] ;
A3: for k being Nat st S1[k] holds
k <= card the carrier of L by NAT_1:43;
consider k being Nat such that
A4: ( S1[k] & ( for n being Nat st S1[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: ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )

thus ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) by A4; :: thesis: verum
end;
then consider k being Element of NAT such that
A5: ( S1[k] & ( for n being Element of NAT st S1[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