take the 0 -wff string of S ; :: thesis: the 0 -wff string of S is wff
thus the 0 -wff string of S is wff ; :: thesis: verum