:: deftheorem defines -maximally-omitting PROOFS_1:def 26 :
for P being non empty ProofSystem
for B, B1 being Subset of P holds
( B1 is B -maximally-omitting iff ( B1 is B -omitting & ( for B2 being Subset of P st B1 c< B2 holds
not B2 is B -omitting ) ) );