per cases ( 2 to_power m >= j or 2 to_power m < j ) ;

suppose A2: 2 to_power m >= j ; :: thesis: ex b₁ being Nat st
( 2 to_power b₁ >= j & b₁ >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b₁ ) )

for k being Nat st 2 to_power k >= j & k >= m holds
k >= m ;
hence ex b₁ being Nat st
( 2 to_power b₁ >= j & b₁ >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b₁ ) ) by A2; :: thesis: verum

end;

suppose A3: 2 to_power m < j ; :: thesis: ex b₁ being Nat st
( 2 to_power b₁ >= j & b₁ >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b₁ ) )

defpred S₁[ Nat] means ( 2 to_power $1 >= j & $1 >= m );
2 to_power m >= m by Th2;
then ( 2 to_power j >= j & j >= m ) by A3, Th2, XXREAL_0:2;
then A4: ex k being Nat st S₁[k] ;
ex k being Nat st
( S₁[k] & ( for l being Nat st S₁[l] holds
l >= k ) ) from NAT_1:sch 5(A4);
hence ex b₁ being Nat st
( 2 to_power b₁ >= j & b₁ >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b₁ ) ) ; :: thesis: verum

end;

end;