theorem Th4: :: MOEBIUS1:4

for n being non prime Nat st n <> 1 holds
ex p being Prime st
( p divides n & p <> n )