let m, n be Nat; ( not m * n = 325 or ( m = 1 & n = 325 ) or ( m = 5 & n = 65 ) or ( m = 13 & n = 25 ) or ( m = 25 & n = 13 ) or ( m = 65 & n = 5 ) or ( m = 325 & n = 1 ) )
assume A1:
m * n = 325
; ( ( m = 1 & n = 325 ) or ( m = 5 & n = 65 ) or ( m = 13 & n = 25 ) or ( m = 25 & n = 13 ) or ( m = 65 & n = 5 ) or ( m = 325 & n = 1 ) )
m divides m * n
;
then
( m = 1 or m = 5 or m = 13 or m = 25 or m = 65 or m = 325 )
by A1, Th22;
hence
( ( m = 1 & n = 325 ) or ( m = 5 & n = 65 ) or ( m = 13 & n = 25 ) or ( m = 25 & n = 13 ) or ( m = 65 & n = 5 ) or ( m = 325 & n = 1 ) )
by A1; verum