theorem Th70: :: NUMBER08:70

for m, n being Nat st (2 |^ m) - (2 |^ n) = 2 holds
( m = 2 & n = 1 )