set Fm = S -formulasOfMaxDepth m;
set FF = AllFormulasOf S;

now

let x be set ; :: thesis: ( x in S -formulasOfMaxDepth m implies x in AllFormulasOf S )
assume x in S -formulasOfMaxDepth m ; :: thesis: x in AllFormulasOf S
then reconsider phi = x as m -wff string of S by DefWff1;
phi in AllFormulasOf S ;
hence x in AllFormulasOf S ; :: thesis: verum

end;

then S -formulasOfMaxDepth m c= AllFormulasOf S by TARSKI:def 3;
hence for b₁ being set st b₁ = (S -formulasOfMaxDepth m) \ (AllFormulasOf S) holds
b₁ is empty ; :: thesis: verum