given q1, q2, q3 being Prime such that A1: q1,q2,q3 are_mutually_distinct and
A2: ( q1 divides p |^ n & q2 divides p |^ n & q3 divides p |^ n ) ; :: according to NUMBER08:def 8 :: thesis: contradiction
( q1 = p & q2 = p & q3 = p ) by A2, Th7, NAT_3:5;
hence contradiction by A1; :: thesis: verum