theorem Th39: :: NUMBER07:39
for m, n being Nat holds
( not m * n = 626 or ( m = 1 & n = 626 ) or ( m = 2 & n = 313 ) or ( m = 313 & n = 2 ) or ( m = 626 & n = 1 ) )