let S be Language; :: thesis: 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#2 S in D & R#5 S in D & R#8 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
X addw (D,num) is D -consistent
let D be RuleSet of S; :: thesis: for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#2 S in D & R#5 S in D & R#8 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
X addw (D,num) is D -consistent
let X be functional set ; :: thesis: for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#2 S in D & R#5 S in D & R#8 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
X addw (D,num) is D -consistent
set EF = ExFormulasOf S;
set G1 = R#1 S;
set G2 = R#2 S;
set G5 = R#5 S;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set L = LettersOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set G8 = R#8 S;
let num be sequence of (ExFormulasOf S); :: thesis: ( D is isotone & R#1 S in D & R#2 S in D & R#5 S in D & R#8 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent implies X addw (D,num) is D -consistent )
set f = (D,num) addw X;
assume A1: ( D is isotone & R#1 S in D & R#2 S in D & R#5 S in D & R#8 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent ) ; :: thesis: X addw (D,num) is D -consistent
set XX = X addw (D,num);

now :: thesis: for Y being finite Subset of (X addw (D,num)) holds Y is D -consistent

let Y be finite Subset of (X addw (D,num)); :: thesis: Y is D -consistent
consider y being set such that
A2: ( y in rng ((D,num) addw X) & Y c= y ) by A1, Lm67, FOMODEL0:65;
consider x being object such that
A3: ( x in dom ((D,num) addw X) & y = ((D,num) addw X) . x ) by A2, FUNCT_1:def 3;
reconsider mm = x as Element of NAT by A3;
( ((D,num) addw X) . mm is D -consistent & Y c= ((D,num) addw X) . mm ) by A3, A2, A1, Th17;
hence Y is D -consistent ; :: thesis: verum

end;

hence X addw (D,num) is D -consistent by Lm51; :: thesis: verum