defpred S₁[ Nat] means for a being set holds #occurrences (a,A) <= $1;
S₁[ len A] by Th54;
then A1: ex n being Nat st S₁[n] ;
consider n being Nat such that
A2: ( S₁[n] & ( for m being Nat st S₁[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