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 b1 being set st b1 = (S -formulasOfMaxDepth m) \ (AllFormulasOf S) holds
b1 is empty ; :: thesis: verum