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

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