let m, n be Nat; :: thesis: for p being Prime holds
( not m * n = p or ( m = 1 & n = p ) or ( m = p & n = 1 ) )
let p be Prime; :: thesis: ( not m * n = p or ( m = 1 & n = p ) or ( m = p & n = 1 ) )
assume A1: m * n = p ; :: thesis: ( ( m = 1 & n = p ) or ( m = p & n = 1 ) )
( m divides m * n & n divides m * n ) ;
then ( ( m = 1 or m = p ) & ( n = 1 or n = p ) ) by A1, INT_2:def 4;
hence ( ( m = 1 & n = p ) or ( m = p & n = 1 ) ) by A1; :: thesis: verum