theorem Th18: :: FOMODEL4:18

for Z being set
for S being Language
for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds
Z is S -witnessed