let X be set ; :: thesis: for S being Language
for phi being wff string of S
for D being RuleSet of S st X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D holds
xnot phi is X,D -provable
let S be Language; :: thesis: for phi being wff string of S
for D being RuleSet of S st X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D holds
xnot phi is X,D -provable
let phi be wff string of S; :: thesis: for D being RuleSet of S st X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D holds
xnot phi is X,D -provable
let D be RuleSet of S; :: thesis: ( X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D implies xnot phi is X,D -provable )
set N = TheNorSymbOf S;
set Y = X \/ {phi};
set r1 = R#1 S;
set r8 = R#8 S;
set psi = xnot phi;
reconsider XX = X null {phi} as Subset of (X \/ {phi}) ;
assume A1: ( X is D -inconsistent & D is isotone & R#1 S in D & R#8 S in D ) ; :: thesis: xnot phi is X,D -provable
then XX is D -inconsistent ;
hence xnot phi is X,D -provable by A1, Lm47, Lm4; :: thesis: verum