let p1 be Prime; :: according to NUMBER08:def 6 :: thesis: ( not p1 divides p |^ 0 or ex r being Prime st
( r <> p1 & r divides p |^ 0 ) )
p |^ 0 = 1 by NEWTON:4;
hence ( not p1 divides p |^ 0 or ex r being Prime st
( r <> p1 & r divides p |^ 0 ) ) by NAT_D:7, INT_2:def 4; :: thesis: verum