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 & R#1 S in D & R#8 S in D & phi is X,D -provable & X is D -consistent holds
X \/ {phi} is D -consistent
let S be Language; :: thesis: for phi being wff string of S
for D being RuleSet of S st D is isotone & R#1 S in D & R#8 S in D & phi is X,D -provable & X is D -consistent holds
X \/ {phi} is D -consistent
let phi be wff string of S; :: thesis: for D being RuleSet of S st D is isotone & R#1 S in D & R#8 S in D & phi is X,D -provable & X is D -consistent holds
X \/ {phi} is D -consistent
let D be RuleSet of S; :: thesis: ( D is isotone & R#1 S in D & R#8 S in D & phi is X,D -provable & X is D -consistent implies X \/ {phi} is D -consistent )
assume A1: ( D is isotone & R#1 S in D & R#8 S in D ) ; :: thesis: ( not phi is X,D -provable or not X is D -consistent or X \/ {phi} is D -consistent )
assume ( phi is X,D -provable & X is D -consistent ) ; :: thesis: X \/ {phi} is D -consistent
then not xnot phi is X,D -provable ;
hence X \/ {phi} is D -consistent by Lm47, A1; :: thesis: verum