set AF = AtomicFormulasOf S;
set Z = S -formulasOfMaxDepth 0;
let w be string of S; :: thesis: ( w is 0 -wff implies w is 0wff )
assume w is 0 -wff ; :: thesis: w is 0wff
then w in S -formulasOfMaxDepth 0 ;
then w in AtomicFormulasOf S by Lm16;
hence w is 0wff ; :: thesis: verum