theorem Th34: :: NUMBER07:34

for m, n being Nat holds
( not m * n = 145 or ( m = 1 & n = 145 ) or ( m = 5 & n = 29 ) or ( m = 29 & n = 5 ) or ( m = 145 & n = 1 ) )