let n be Nat; :: thesis: ( n is trivial & n is square-containing implies n is zero )
assume A1: ( n is trivial & n is square-containing ) ; :: thesis: n is zero
then ( n = 0 or n = 1 ) by NAT_2:def 1;
hence n is zero by A1, Th22; :: thesis: verum