:: deftheorem Def17 defines Omit PROOFS_1:def 25 :
for P being non empty ProofSystem
for B being Subset of P
for b₃ being Subset-Family of P holds
( b₃ = Omit (P,B) iff for B1 being Subset of P holds
( B1 in b₃ iff B1 is B -omitting ) );