not 3 is square by PEPIN:41;
hence not for b₁ being Element of NAT holds b₁ is square ; :: thesis: verum