thus ( x = 0 implies ex y being non zero Nat st y = 1 ) ; :: thesis:
thus ( not x = 0 implies ex y being non zero Nat ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & y = n + 1 ) ) :: thesis:

assume x <> 0 ; :: thesis:
then consider n being Nat such that
A1: ( 2 to_power n <= x & x < 2 to_power (n + 1) ) by LM001;
take y = n + 1; :: thesis:
thus ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & y = n + 1 ) by A1; :: thesis:

end;