theorem Th29: :: NUMBER07:29

for m, n being Nat holds
( not m * n = 26 or ( m = 1 & n = 26 ) or ( m = 2 & n = 13 ) or ( m = 13 & n = 2 ) or ( m = 26 & n = 1 ) )