let S be Language; :: thesis: for D being RuleSet of S holds AllFormulasOf S is D -expanded
let D be RuleSet of S; :: thesis: AllFormulasOf S is D -expanded
set AF = AllFormulasOf S;

now

let x be set ; :: thesis: ( x is AllFormulasOf S,D -provable implies {x} c= AllFormulasOf S )
assume x is AllFormulasOf S,D -provable ; :: thesis: {x} c= AllFormulasOf S
then reconsider xx = x as wff string of S by Lm33;
consider m being Nat such that
C0: xx is m -wff by FOMODEL2:def 25;
xx in AllFormulasOf S by C0;
hence {x} c= AllFormulasOf S by ZFMISC_1:31; :: thesis: verum

end;

hence AllFormulasOf S is D -expanded by DefExpanded; :: thesis: verum