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

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