set w = the 0 -wff string of S;
the 0 -wff string of S in AllFormulasOf S ;
hence not AllFormulasOf S is empty ; :: thesis: verum