:: deftheorem defines -omitting PROOFS_1:def 23 :
for P being non empty ProofSystem
for B, B1 being Subset of P holds
( B1 is B -omitting iff ex a being object st
( a in B & not P \/ B1 |- a ) );