:: deftheorem defines Omit PROOFS_1:def 24 :
for P being non empty ProofSystem
for B being Subset of P holds Omit (P,B) = { B1 where B1 is Subset of P : B1 is B -omitting } ;