defpred S_{1}[ Nat] means for a being set holds #occurrences (a,A) <= $1;

S_{1}[ len A]
by Th54;

then A1: ex n being Nat st S_{1}[n]
;

consider n being Nat such that

A2: ( S_{1}[n] & ( for m being Nat st S_{1}[m] holds

n <= m ) ) from NAT_1:sch 5(A1);

take n ; :: thesis: ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

n <= n ) )

thus ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

n <= n ) ) by A2; :: thesis: verum

S

then A1: ex n being Nat st S

consider n being Nat such that

A2: ( S

n <= m ) ) from NAT_1:sch 5(A1);

take n ; :: thesis: ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

n <= n ) )

thus ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds

n <= n ) ) by A2; :: thesis: verum