let P be non empty ProofSystem ; :: thesis: 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 )
let B be Subset of P; :: thesis: 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 )
let F be finite Subset of P; :: thesis: ( B is F -omitting implies ex B1 being Subset of P st
( B c= B1 & B1 is F -maximally-omitting ) )
assume A1: B is F -omitting ; :: thesis: ex B1 being Subset of P st
( B c= B1 & B1 is F -maximally-omitting )
set A = the Axioms of P;
set R = the Rules of P;
set Q = P \/ B;
reconsider G = F as Subset of (P \/ B) ;
set Om = Omit ((P \/ B),G);
A2: for C1 being Subset of (P \/ B)
for B1 being Subset of P st B1 = C1 \/ B holds
( C1 in Omit ((P \/ B),G) iff B1 is F -omitting )

proof

let C1 be Subset of (P \/ B); :: thesis: for B1 being Subset of P st B1 = C1 \/ B holds
( C1 in Omit ((P \/ B),G) iff B1 is F -omitting )
let B1 be Subset of P; :: thesis: ( B1 = C1 \/ B implies ( C1 in Omit ((P \/ B),G) iff B1 is F -omitting ) )
assume B1 = C1 \/ B ; :: thesis: ( C1 in Omit ((P \/ B),G) iff B1 is F -omitting )
then A3: the Axioms of ((P \/ B) \/ C1) = the Axioms of P \/ B1 by XBOOLE_1:4;
thus ( C1 in Omit ((P \/ B),G) implies B1 is F -omitting ) :: thesis: ( B1 is F -omitting implies C1 in Omit ((P \/ B),G) )

proof

assume C1 in Omit ((P \/ B),G) ; :: thesis: B1 is F -omitting
then C1 is G -omitting by Def17;
then consider a being object such that
A4: ( a in G & not (P \/ B) \/ C1 |- a ) ;
thus B1 is F -omitting by A3, A4; :: thesis: verum

end;

assume B1 is F -omitting ; :: thesis: C1 in Omit ((P \/ B),G)
then consider a being object such that
A6: ( a in F & not P \/ B1 |- a ) ;
C1 is G -omitting by A3, A6;
hence C1 in Omit ((P \/ B),G) ; :: thesis: verum

end;

A10: not Omit ((P \/ B),G) is empty

proof

set E = {} the carrier of (P \/ B);
B = ({} the carrier of (P \/ B)) \/ B ;
hence not Omit ((P \/ B),G) is empty by A1, A2; :: thesis: verum

end;

then consider Y being Element of Omit ((P \/ B),G) such that
A11: for Z being Element of Omit ((P \/ B),G) holds not Y c< Z by Th60;
A12: Y in Omit ((P \/ B),G) by A10;
then reconsider B1 = B \/ Y as Subset of P by XBOOLE_1:8;
take B1 ; :: thesis: ( B c= B1 & B1 is F -maximally-omitting )
thus B c= B1 by XBOOLE_1:7; :: thesis: B1 is F -maximally-omitting
thus B1 is F -omitting by A2, A12; :: according to PROOFS_1:def 26 :: thesis: for B2 being Subset of P st B1 c< B2 holds
not B2 is F -omitting
let B2 be Subset of P; :: thesis: ( B1 c< B2 implies not B2 is F -omitting )
reconsider C2 = B2 as Subset of (P \/ B) ;
assume A15: B1 c< B2 ; :: thesis: not B2 is F -omitting
assume A16: B2 is F -omitting ; :: thesis: contradiction
B c< B2 by A15, XBOOLE_1:7, XBOOLE_1:59;
then B2 = B \/ C2 by XBOOLE_1:12;
then A18: C2 in Omit ((P \/ B),G) by A2, A16;
Y c= B1 by XBOOLE_1:7;
hence contradiction by A11, A15, A18, XBOOLE_1:59; :: thesis: verum