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 :: thesis: for x being set st x is AllFormulasOf S,D -provable holds
{x} c= AllFormulasOf S

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 Lm25;
consider m being Nat such that
A1: xx is m -wff by FOMODEL2:def 25;
xx in AllFormulasOf S by A1;
hence {x} c= AllFormulasOf S by ZFMISC_1:31; :: thesis: verum

end;

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