let P be non empty ProofSystem ; :: thesis: for B, B1 being Subset of P st B is inconsistent holds
( B1 is consistent iff B1 is B -omitting )
let B, B1 be Subset of P; :: thesis: ( B is inconsistent implies ( B1 is consistent iff B1 is B -omitting ) )
set A = the Axioms of P;
set R = the Rules of P;
assume B is inconsistent ; :: thesis: ( B1 is consistent iff B1 is B -omitting )
then A1: P \/ B is inconsistent ;
thus ( B1 is consistent implies B1 is B -omitting ) :: thesis: ( B1 is B -omitting implies B1 is consistent )

proof

assume B1 is consistent ; :: thesis: B1 is B -omitting
then P \/ B1 is consistent ;
then consider a being object such that
A2: a in P \/ B1 and
A3: not P \/ B1 |- a ;
a in P \/ B by A2;
then A5: P \/ B |- a by A1;
assume A7: not B1 is B -omitting ; :: thesis: contradiction
for b being object st b in the Axioms of P \/ B holds
the Axioms of P \/ B1, the Rules of P |- b

proof

let b be object ; :: thesis: ( b in the Axioms of P \/ B implies the Axioms of P \/ B1, the Rules of P |- b )
assume b in the Axioms of P \/ B ; :: thesis: the Axioms of P \/ B1, the Rules of P |- b

per cases then ( b in the Axioms of P or b in B ) by XBOOLE_0:def 3;

suppose b in the Axioms of P ; :: thesis: the Axioms of P \/ B1, the Rules of P |- b

then b in the Axioms of P \/ B1 by XBOOLE_0:def 3;
hence the Axioms of P \/ B1, the Rules of P |- b by Th46; :: thesis: verum

end;

suppose b in B ; :: thesis: the Axioms of P \/ B1, the Rules of P |- b

then P \/ B1 |- b by A7;
hence the Axioms of P \/ B1, the Rules of P |- b ; :: thesis: verum

end;

end;

end;

hence contradiction by A3, A5, Th53; :: thesis: verum

end;

assume B1 is B -omitting ; :: thesis: B1 is consistent
then consider a being object such that
A11: a in B and
A12: not P \/ B1 |- a ;
a in P \/ B1 by A11;
then P \/ B1 is consistent by A12;
hence B1 is consistent ; :: thesis: verum