A1: 2 ^2 = 2 * 2 by SQUARE_1:def 1;
4 is non trivial Element of NAT by NAT_2:def 1;
hence not for b₁ being square Element of NAT holds b₁ is trivial by A1; :: thesis: verum