set A = the Axioms of P;
set Obj = the carrier of P;
set R = the Rules of P;
set O = Omit (P,F);
let B be Subset of P; :: according to PROOFS_1:def 29 :: thesis: ( B in Omit (P,F) iff for S being finite Subset of B holds S in Omit (P,F) )
thus ( B in Omit (P,F) implies for S being finite Subset of B holds S in Omit (P,F) ) :: thesis: ( ( for S being finite Subset of B holds S in Omit (P,F) ) implies B in Omit (P,F) )

proof

set PB = P \/ B;
assume B in Omit (P,F) ; :: thesis: for S being finite Subset of B holds S in Omit (P,F)
then A1: B is F -omitting by Def17;
let S be finite Subset of B; :: thesis: S in Omit (P,F)
( S c= B & B c= the carrier of P ) ;
then S c= the carrier of P ;
then reconsider T = S as Subset of P ;
T is F -omitting by A1, Th59;
hence S in Omit (P,F) ; :: thesis: verum

end;

assume A10: for S being finite Subset of B holds S in Omit (P,F) ; :: thesis: B in Omit (P,F)
assume not B in Omit (P,F) ; :: thesis: contradiction
then A11: not B is F -omitting ;
for a being object st a in F holds
the Axioms of P \/ B, the Rules of P |- a

proof

let a be object ; :: thesis: ( a in F implies the Axioms of P \/ B, the Rules of P |- a )
assume a in F ; :: thesis: the Axioms of P \/ B, the Rules of P |- a
then P \/ B |- a by A11;
hence the Axioms of P \/ B, the Rules of P |- a ; :: thesis: verum

end;

then consider S1 being Formula-finset such that
A12: F c= S1 and
A13: S1 is the Axioms of P \/ B, the Rules of P -derivable by Th47;
set S2 = B /\ S1;
( ( the Axioms of P \/ B) /\ S1 = ( the Axioms of P /\ S1) \/ (B /\ S1) & the Axioms of P /\ S1 c= the Axioms of P ) by XBOOLE_1:17, XBOOLE_1:23;
then S1 is the Axioms of P \/ (B /\ S1), the Rules of P -derivable by A13, Th48, XBOOLE_1:9;
then for a being object st a in F holds
the Axioms of P \/ (B /\ S1), the Rules of P |- a by A12;
then for a being object st a in F holds
P \/ (B /\ S1) |- a ;
then not B /\ S1 is F -omitting ;
then A15: not B /\ S1 in Omit (P,F) by Def17;
B /\ S1 is finite Subset of B by XBOOLE_1:17;
hence contradiction by A10, A15; :: thesis: verum