let X be set ; :: thesis: for S being Language
for phi being wff string of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & phi is X,D -provable & not X is D -inconsistent holds
not X \/ {phi} is D -inconsistent
let S be Language; :: thesis: for phi being wff string of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & phi is X,D -provable & not X is D -inconsistent holds
not X \/ {phi} is D -inconsistent
let phi be wff string of S; :: thesis: for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & phi is X,D -provable & not X is D -inconsistent holds
not X \/ {phi} is D -inconsistent
let D be RuleSet of S; :: thesis: ( D is isotone & R1 S in D & R8 S in D & phi is X,D -provable & not X is D -inconsistent implies not X \/ {phi} is D -inconsistent )
assume B0: ( D is isotone & R1 S in D & R8 S in D ) ; :: thesis: ( not phi is X,D -provable or X is D -inconsistent or not X \/ {phi} is D -inconsistent )
assume ( phi is X,D -provable & not X is D -inconsistent ) ; :: thesis: not X \/ {phi} is D -inconsistent
then not xnot phi is X,D -provable by DefInc;
hence not X \/ {phi} is D -inconsistent by Lm2b, B0; :: thesis: verum