set X = S -formulasOfMaxDepth m;
set phi = the m -wff string of S;
the m -wff string of S in S -formulasOfMaxDepth m by Def23;
hence not S -formulasOfMaxDepth m is empty ; :: thesis: verum