let it1, it2 be Element of NAT ; :: thesis: ( it1 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it1 ) & it2 is_sufficiently_large_for C & ( for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it2 ) implies it1 = it2 )
assume that
A3: it1 is_sufficiently_large_for C and
A4: for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it1 and
A5: it2 is_sufficiently_large_for C and
A6: for j being Element of NAT st j is_sufficiently_large_for C holds
j >= it2 ; :: thesis: it1 = it2
A7: it2 <= it1 by A3, A6;
it1 <= it2 by A4, A5;
hence it1 = it2 by A7, XXREAL_0:1; :: thesis: verum