let n be Nat; :: 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 |^ 2 divides n by A2, WSIERP_1:1;
( m <> 1 ^2 & m <> 0 ^2 ) by A1, A2, NAT_2:28;
hence n is square-containing by A3, Th20; :: thesis: verum