let m, n be Nat; :: thesis: ( not m * n = 82 or ( m = 1 & n = 82 ) or ( m = 2 & n = 41 ) or ( m = 41 & n = 2 ) or ( m = 82 & n = 1 ) )
assume A1: m * n = 82 ; :: thesis: ( ( m = 1 & n = 82 ) or ( m = 2 & n = 41 ) or ( m = 41 & n = 2 ) or ( m = 82 & n = 1 ) )
m divides m * n ;
then ( m = 1 or m = 2 or m = 41 or m = 82 ) by A1, Th18;
hence ( ( m = 1 & n = 82 ) or ( m = 2 & n = 41 ) or ( m = 41 & n = 2 ) or ( m = 82 & n = 1 ) ) by A1; :: thesis: verum