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