let X be set ; :: thesis:
let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
set EF = ExFormulasOf S;
set L = LettersOf S;
set FF = AllFormulasOf S;
let num be Function of NAT,(AllFormulasOf S); :: thesis:
set XX = (D,num) CompletionOf X;
set G1 = R1 S;
set G8 = R8 S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set f = (D,num) AddFormulasTo X;
assume B0: ( D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent ) ; :: thesis:
B1: for nn, mm being Element of NAT st mm in dom ((D,num) AddFormulasTo X) & nn in dom ((D,num) AddFormulasTo X) & nn < mm holds
((D,num) AddFormulasTo X) . nn c= ((D,num) AddFormulasTo X) . mm

proof

let nn, mm be Element of NAT ; :: thesis:
set m = mm;
set n = nn;
assume ( mm in dom ((D,num) AddFormulasTo X) & nn in dom ((D,num) AddFormulasTo 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) AddFormulasTo X) . nn c= ((D,num) AddFormulasTo X) . (nn + k) by B0, Lm4;
hence ((D,num) AddFormulasTo X) . nn c= ((D,num) AddFormulasTo X) . mm ; :: thesis:

end;

now

let Y be finite Subset of ((D,num) CompletionOf X); :: thesis:
consider kk being Element of NAT such that
C0: Y c= ((D,num) AddFormulasTo X) . kk by B1, HENMODEL:3;
not ((D,num) AddFormulasTo X) . kk is D -inconsistent by B0, Lm4;
hence not Y is D -inconsistent by C0, Th16; :: thesis:

end;

hence not (D,num) CompletionOf X is D -inconsistent by Lm1; :: thesis: