let n be natural number ; :: thesis: ( n is square & not n is trivial implies n is square-containing )
assume A1: ( n is square & not n is trivial ) ; :: thesis: n is square-containing
then consider m being Nat such that
A2: n = m ^2 by PYTHTRIP:def 3;
A3: m <> 1 ^2 by A1, A2, NAT_2:30;
A4: m <> 0 ^2 by A1, A2, NAT_2:30;
n = m * m by A2;
then m |^ 2 divides n by WSIERP_1:2;
hence n is square-containing by A3, A4, Th20; :: thesis: verum