let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
let X be functional set ; :: thesis:
set EF = ExFormulasOf S;
set L = LettersOf S;
set G1 = R#1 S;
let num be Function of NAT,(ExFormulasOf S); :: thesis:
set XX = X addw (D,num);
set f = (D,num) addw X;
set G2 = R#2 S;
set G5 = R#5 S;
set G8 = R#8 S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
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:
A2: for nn, mm being Element of NAT st mm in dom ((D,num) addw X) & nn in dom ((D,num) addw X) & nn < mm holds
((D,num) addw X) . nn c= ((D,num) addw X) . mm

let nn, mm be Element of NAT ; :: thesis:
set m = mm;
set n = nn;
assume ( mm in dom ((D,num) addw X) & nn in dom ((D,num) addw X) & nn < mm ) ; :: thesis:
then nn - nn <= mm - nn by XREAL_1:9;
then 0 <= mm - nn ;
then reconsider k = mm - nn as Nat ;
((D,num) addw X) . nn c= ((D,num) addw X) . (nn + k) by Th17, A1;
hence ((D,num) addw X) . nn c= ((D,num) addw X) . mm ; :: thesis:

end;

let Y be finite Subset of (X addw (D,num)); :: thesis:
consider kk being Element of NAT such that
A3: Y c= ((D,num) addw X) . kk by A2, HENMODEL:3;
((D,num) addw X) . kk is D -consistent by A1, Th17;
hence Y is D -consistent by A3, Th15; :: thesis:

end;