theorem :: NUMBER10:54

{ [x,y] where x, y is positive Nat : (2 |^ x) - 1 = y ^2 } = {[1,1]}