set X = S -formulasOfMaxDepth m;
set Y = S -formulasOfMaxDepth (m + n);
A1: S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n) by Lm15;
let w be string of S; :: thesis: ( w is m + (0 * n) -wff implies w is m + n -wff )
assume w is m + (0 * n) -wff ; :: thesis: w is m + n -wff
then w in S -formulasOfMaxDepth m ;
hence w is m + n -wff by A1; :: thesis: verum