set TS = (SqF n) |^ 2;
(SqF n) |^ 2 = TSqF n by Cosik;
hence for b₁ being Nat st b₁ = n div ((SqF n) |^ 2) holds
not b₁ is square-containing ; :: thesis: verum