let k, l be Nat; :: thesis: ( (2 |^ k) - (2 |^ l) = 2 & k >= 2 & l >= 1 implies ( k = 2 & l = 1 ) )
assume A0: (2 |^ k) - (2 |^ l) = 2 ; :: thesis: ( not k >= 2 or not l >= 1 or ( k = 2 & l = 1 ) )
assume k >= 2 ; :: thesis: ( not l >= 1 or ( k = 2 & l = 1 ) )
then k - 1 >= 2 - 1 by XREAL_1:9;
then a1: k - 1 >= 1 ;
then (k -' 1) + 1 = k by NAT_D:43;
then A1: (2 |^ (k -' 1)) * 2 = 2 |^ k by NEWTON:6;
A5: k - 1 >= 0 by a1;
assume l >= 1 ; :: thesis: ( k = 2 & l = 1 )
then A3: l - 1 >= 0 ;
then l -' 1 = l - 1 by XREAL_0:def 2;
then (l -' 1) + 1 = l ;
then (2 |^ (l -' 1)) * 2 = 2 |^ l by NEWTON:6;
then 2 |^ (k -' 1) = (2 |^ (l -' 1)) + 1 by A0, A1;

per cases then ( ( 2 |^ (k -' 1) is even & 2 |^ (l -' 1) is odd ) or ( 2 |^ (k -' 1) is odd & 2 |^ (l -' 1) is even ) ) ;

suppose ( 2 |^ (k -' 1) is even & 2 |^ (l -' 1) is odd ) ; :: thesis: ( k = 2 & l = 1 )

then ( not k -' 1 is empty & l -' 1 is zero ) ;
then l - 1 = 0 by A3, XREAL_0:def 2;
then A4: l = 1 ;
2 |^ k = 2 + (2 |^ l) by A0
.= 4 by A4 ;
then 2 to_power k = 2 to_power 2 by POWER:60;
hence ( k = 2 & l = 1 ) by A4, POWER:50; :: thesis: verum

end;

suppose ( 2 |^ (k -' 1) is odd & 2 |^ (l -' 1) is even ) ; :: thesis: ( k = 2 & l = 1 )

then ( k -' 1 is zero & not l -' 1 is empty ) ;
then k - 1 = 0 by A5, XREAL_0:def 2;
then A4: k = 1 ;
2 |^ l = (2 |^ k) - 2 by A0
.= 0 by A4 ;
hence ( k = 2 & l = 1 ) ; :: thesis: verum

end;

end;