theorem Th31: :: NUMBER07:31
for m, n being Nat holds
( not m * n = 65 or ( m = 1 & n = 65 ) or ( m = 5 & n = 13 ) or ( m = 13 & n = 5 ) or ( m = 65 & n = 1 ) )