let X be set ; 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; 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; 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); ( 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 )
; (D,num) CompletionOf X is D -consistent
now 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);
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
;
verum end;
hence
(D,num) CompletionOf X is D -consistent
by Lm51; verum