let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds
(D,num) CompletionOf X is D -consistent
let S be Language; :: thesis: for D being RuleSet of S
for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds
(D,num) CompletionOf X is D -consistent
let D be RuleSet of S; :: thesis: for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds
(D,num) CompletionOf X is D -consistent
set EF = ExFormulasOf S;
set L = LettersOf S;
set FF = AllFormulasOf S;
let num be sequence of (AllFormulasOf S); :: thesis: ( D is isotone & R#1 S in D & R#8 S in D & X is D -consistent implies (D,num) CompletionOf X is D -consistent )
set XX = (D,num) CompletionOf X;
set G1 = R#1 S;
set G8 = R#8 S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set f = (D,num) AddFormulasTo X;
assume A1: ( D is isotone & R#1 S in D & R#8 S in D & X is D -consistent ) ; :: thesis: (D,num) CompletionOf X is D -consistent

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

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

end;

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