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

now :: thesis: for x being object st x in S -formulasOfMaxDepth m holds
x in AllFormulasOf S

let x be object ; :: 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 Def23;
phi in AllFormulasOf S ;
hence x in AllFormulasOf S ; :: thesis: verum

end;

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