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

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