let m, n be Nat; ( not m * n = 50 or ( m = 1 & n = 50 ) or ( m = 2 & n = 25 ) or ( m = 5 & n = 10 ) or ( m = 10 & n = 5 ) or ( m = 25 & n = 2 ) or ( m = 50 & n = 1 ) )
assume A1:
m * n = 50
; ( ( m = 1 & n = 50 ) or ( m = 2 & n = 25 ) or ( m = 5 & n = 10 ) or ( m = 10 & n = 5 ) or ( m = 25 & n = 2 ) or ( m = 50 & n = 1 ) )
m divides m * n
;
then
( m = 1 or m = 2 or m = 5 or m = 10 or m = 25 or m = 50 )
by A1, Th16;
hence
( ( m = 1 & n = 50 ) or ( m = 2 & n = 25 ) or ( m = 5 & n = 10 ) or ( m = 10 & n = 5 ) or ( m = 25 & n = 2 ) or ( m = 50 & n = 1 ) )
by A1; verum