theorem Th20: :: MOEBIUS1:20

for n being Nat st ex p being non zero Nat st
( p <> 1 & p |^ 2 divides n ) holds
n is square-containing