theorem Diff2A: :: NUMBER18:33

for k, l being Nat st (2 |^ k) - (2 |^ l) = 2 & k >= 2 & l >= 1 holds
( k = 2 & l = 1 )