let p, q be Nat; :: thesis: ( 2 to_power p >= j & p >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= p ) & 2 to_power q >= j & q >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= q ) implies p = q )
assume ( 2 to_power p >= j & p >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= p ) & 2 to_power q >= j & q >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= q ) ) ; :: thesis: p = q
then ( p >= q & q >= p ) ;
hence p = q by XXREAL_0:1; :: thesis: verum