0 * 0 = 0 ^2 ;
hence ex b₁ being Nat st b₁ is square ; :: thesis: verum