take the non 0wff the non zero Nat -wff exal string of S ; :: thesis: not the non 0wff the non zero Nat -wff exal string of S is 0wff
thus not the non 0wff the non zero Nat -wff exal string of S is 0wff ; :: thesis: verum