theorem :: FOMODEL4:12

for X, x being set
for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S by Lm25;