let n1, n2 be Nat; :: thesis: ( ( for a being set holds #occurrences (a,A) <= n1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n1 <= n ) & ( for a being set holds #occurrences (a,A) <= n2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n2 <= n ) implies n1 = n2 )
assume that
A3: ( ( for a being set holds #occurrences (a,A) <= n1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n1 <= n ) ) and
A4: ( ( for a being set holds #occurrences (a,A) <= n2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n2 <= n ) ) ; :: thesis: n1 = n2
( n1 <= n2 & n2 <= n1 ) by A3, A4;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum