let P be non empty ProofSystem ; :: thesis: for B, B1, B2 being Subset of P st B1 is B -omitting & B2 c= B1 holds
B2 is B -omitting
let B, B1, B2 be Subset of P; :: thesis: ( B1 is B -omitting & B2 c= B1 implies B2 is B -omitting )
set A = the Axioms of P;
set R = the Rules of P;
assume that
A1: B1 is B -omitting and
A2: B2 c= B1 ; :: thesis: B2 is B -omitting
consider a being object such that
A3: a in B and
A4: not P \/ B1 |- a by A1;
take a ; :: according to PROOFS_1:def 23 :: thesis: ( a in B & not P \/ B2 |- a )
( the Axioms of P \/ B1 is Extension of the Axioms of P \/ B2 & the Rules of P is Extension of the Rules of P ) by A2, Def11, Def12, XBOOLE_1:9;
hence ( a in B & not P \/ B2 |- a ) by A3, A4, Th54; :: thesis: verum