let m, n be Nat; :: thesis: ( (2 |^ m) - (2 |^ n) = 2 implies ( m = 2 & n = 1 ) )
assume A1: (2 |^ m) - (2 |^ n) = 2 ; :: thesis: ( m = 2 & n = 1 )

now :: thesis: not n >= m

assume n >= m ; :: thesis: contradiction
then (2 |^ m) - (2 |^ n) <= (2 |^ n) - (2 |^ n) by XREAL_1:9, PREPOWER:93;
hence contradiction by A1; :: thesis: verum

end;

then consider k being Nat such that
A2: m = n + k by NAT_1:10;

per cases ( 1 <= n or n < 1 ) ;

suppose 1 <= n ; :: thesis: ( m = 2 & n = 1 )

then reconsider n1 = n - 1 as Element of NAT by INT_1:3;
A3: 2 |^ (n + k) = (2 |^ n) * (2 |^ k) by NEWTON:8;
2 |^ n = 2 |^ (n1 + 1)
.= (2 |^ n1) * 2 by NEWTON:6 ;
then ((2 |^ n1) * 2) * ((2 |^ k) - 1) = 2 * 1 by A1, A2, A3;
then (2 |^ n1) * ((2 |^ k) - 1) = 1 ;
then ( 2 |^ n1 = 1 & (2 |^ k) - 1 = 1 ) by NAT_1:15;
then ( 2 |^ n1 = 2 |^ 0 & 2 |^ k = 2 |^ 1 ) by NEWTON:4;
then ( n1 = 0 & k = 1 ) by PEPIN:30;
hence ( m = 2 & n = 1 ) by A2; :: thesis: verum

end;

suppose n < 1 ; :: thesis: ( m = 2 & n = 1 )

then A4: n = 0 by NAT_1:14;
then m = 0 by A1;
hence ( m = 2 & n = 1 ) by A1, A4; :: thesis: verum

end;

end;