4 = 2 ^2 ;
then ( not 4 is zero & 4 is square ) ;
hence ex b₁ being Nat st
( not b₁ is zero & b₁ is square & not b₁ is trivial ) by NAT_2:28; :: thesis: verum