( 1 * 1 = 1 ^2 & 0 * 0 = 0 ^2 ) ;
hence for b₁ being Nat st b₁ is trivial holds
b₁ is square by NAT_2:def 1; :: thesis: verum