per cases ( 2 to_power m >= j or 2 to_power m < j ) ;
suppose A1: 2 to_power m >= j ; :: thesis: ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) )
for k being Nat st 2 to_power k >= j & k >= m holds
k >= m ;
hence ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) ) by A1; :: thesis: verum
end;
suppose A2: 2 to_power m < j ; :: thesis: ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) )
defpred S1[ Nat] means ( 2 to_power $1 >= j & $1 >= m );
2 to_power m >= m by Th2;
then A3: j >= m by A2, XXREAL_0:2;
2 to_power j >= j by Th2;
then A4: ex k being Nat st S1[k] by A3;
ex k being Nat st
( S1[k] & ( for l being Nat st S1[l] holds
l >= k ) ) from NAT_1:sch 5(A4);
hence ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) ) ; :: thesis: verum
end;
end;