let k, m be Nat; :: thesis: for X being 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) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent )
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) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m 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) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m 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) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent )
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) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent ) )
set f = (D,num) AddFormulasTo X;
assume A1: ( D is isotone & R#1 S in D & R#8 S in D ) ; :: thesis: ( not X is D -consistent or ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent ) )
assume A2: X is D -consistent ; :: thesis: ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent )
defpred S₁[ Nat] means ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + $1) & ((D,num) AddFormulasTo X) . $1 is D -consistent );
A3: S₁[ 0 ] by A2, Def74;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set fkn1 = (D,(num . (k + n))) AddFormulaTo (((D,num) AddFormulasTo X) . (k + n));
set fkn = ((D,num) AddFormulasTo X) . (k + n);
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: (((D,num) AddFormulasTo X) . (k + n)) \ ((D,(num . (k + n))) AddFormulaTo (((D,num) AddFormulasTo X) . (k + n))) = {} ;
((D,num) AddFormulasTo X) . (k + (n + 1)) = ((D,num) AddFormulasTo X) . ((k + n) + 1)
.= (D,(num . (k + n))) AddFormulaTo (((D,num) AddFormulasTo X) . (k + n)) by Def74 ;
then ((D,num) AddFormulasTo X) . (k + n) c= ((D,num) AddFormulasTo X) . (k + (n + 1)) by A6, XBOOLE_1:37;
hence ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + (n + 1)) by XBOOLE_1:1, A5; :: thesis: ((D,num) AddFormulasTo X) . (n + 1) is D -consistent
reconsider phii = num . n as Element of AllFormulasOf S ;
reconsider phi = phii as wff string of S ;
reconsider psi = xnot phi as wff string of S ;
reconsider psii = psi as Element of AllFormulasOf S by FOMODEL2:16;
set fn = ((D,num) AddFormulasTo X) . n;
set fN = (D,(num . n)) AddFormulaTo (((D,num) AddFormulasTo X) . n);
defpred S₂[] means xnot phii is ((D,num) AddFormulasTo X) . n,D -provable ;
A7: ((D,num) AddFormulasTo X) . (n + 1) = (D,(num . n)) AddFormulaTo (((D,num) AddFormulasTo X) . n) by Def74;

per cases ( not S₂[] or S₂[] ) ;

suppose A8: not S₂[] ; :: thesis: ((D,num) AddFormulasTo X) . (n + 1) is D -consistent

then (((D,num) AddFormulasTo X) . n) \/ {phii} is D -consistent by A1, Lm47;
hence ((D,num) AddFormulasTo X) . (n + 1) is D -consistent by A7, A8, Def73; :: thesis: verum

end;

suppose A9: S₂[] ; :: thesis: ((D,num) AddFormulasTo X) . (n + 1) is D -consistent

then (((D,num) AddFormulasTo X) . n) \/ {(xnot phii)} is D -consistent by Lm71, A1, A5;
hence ((D,num) AddFormulasTo X) . (n + 1) is D -consistent by A7, A9, Def73; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent ) ; :: thesis: verum