theorem Th61: :: PROOFS_1:22

for P being non empty ProofSystem
for B being Subset of P
for F being finite Subset of P st B is F -omitting holds
ex B1 being Subset of P st
( B c= B1 & B1 is F -maximally-omitting )