theorem SFS: :: NEWTON06:8

for a being Nat holds
( ( a is square & a is square-free ) iff a = 1 )