let k, m be Nat; :: thesis: for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent holds
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent )
let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent holds
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent )
let S be Language; :: thesis: for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent holds
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent )
let D be RuleSet of S; :: thesis: for num being Function of NAT,(AllFormulasOf S) st D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent holds
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent )
set FF = AllFormulasOf S;
let num be Function of NAT,(AllFormulasOf S); :: thesis: ( D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent implies ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent ) )
set f = (D,num) AddFormulasTo X;
assume B10: ( D is isotone & R1 S in D & R8 S in D ) ; :: thesis: ( X is D -inconsistent or ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent ) )
assume B11: not X is D -inconsistent ; :: thesis: ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent )
defpred S₁[ Nat] means ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + $1) & not ((D,num) AddFormulasTo X) . $1 is D -inconsistent );
B0: S₁[ 0 ] by B11, DefAdd2;
B1: 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 C1: S₁[n] ; :: thesis: S₁[n + 1]
CC0: (((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 DefAdd2 ;
then ((D,num) AddFormulasTo X) . (k + n) c= ((D,num) AddFormulasTo X) . (k + (n + 1)) by CC0, XBOOLE_1:37;
hence ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + (n + 1)) by C1, XBOOLE_1:1; :: thesis: not ((D,num) AddFormulasTo X) . (n + 1) is D -inconsistent
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 ;
C2: ((D,num) AddFormulasTo X) . (n + 1) = (D,(num . n)) AddFormulaTo (((D,num) AddFormulasTo X) . n) by DefAdd2;

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

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

then not (((D,num) AddFormulasTo X) . n) \/ {phii} is D -inconsistent by B10, Lm2b;
hence not ((D,num) AddFormulasTo X) . (n + 1) is D -inconsistent by C2, D0, DefAdd1; :: thesis: verum

end;

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

then not (((D,num) AddFormulasTo X) . n) \/ {(xnot phii)} is D -inconsistent by Lm3, B10, C1;
hence not ((D,num) AddFormulasTo X) . (n + 1) is D -inconsistent by C2, D0, DefAdd1; :: thesis: verum

end;

end;

end;

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