let B be set ; :: thesis: for R being Rule
for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) holds
ex S1 being Formula-finset st
( S c= S1 & S1 is B,R -derivable )
let R be Rule; :: thesis: for S being Formula-finset st ( for a being object st a in S holds
B,R |- a ) holds
ex S1 being Formula-finset st
( S c= S1 & S1 is B,R -derivable )
let S be Formula-finset; :: thesis: ( ( for a being object st a in S holds
B,R |- a ) implies ex S1 being Formula-finset st
( S c= S1 & S1 is B,R -derivable ) )
assume A1: for a being object st a in S holds
B,R |- a ; :: thesis: ex S1 being Formula-finset st
( S c= S1 & S1 is B,R -derivable )
defpred S₁[ set ] means ex S1 being Formula-finset st
( $1 c= S1 & S1 is B,R -derivable );
A2: S is finite ;
A10: S₁[ {} ]

proof

set P = <*> {};
take rng (<*> {}) ; :: thesis: ( {} c= rng (<*> {}) & rng (<*> {}) is B,R -derivable )
<*> {} is B,R -correct ;
hence ( {} c= rng (<*> {}) & rng (<*> {}) is B,R -derivable ) ; :: thesis: verum

end;

A20: for x, B1 being set st x in S & B1 c= S & S₁[B1] holds
S₁[B1 \/ {x}]

proof

let x, B1 be set ; :: thesis: ( x in S & B1 c= S & S₁[B1] implies S₁[B1 \/ {x}] )
assume that
A21: x in S and
B1 c= S and
A23: S₁[B1] ; :: thesis: S₁[B1 \/ {x}]
reconsider t = x as Formula ;
consider S1 being Formula-finset such that
A24: t in S1 and
A25: S1 is B,R -derivable by A1, A21, Th45;
consider S2 being Formula-finset such that
A26: B1 c= S2 and
A27: S2 is B,R -derivable by A23;
take S1 \/ S2 ; :: thesis: ( B1 \/ {x} c= S1 \/ S2 & S1 \/ S2 is B,R -derivable )
{x} c= S1 by A24, TARSKI:def 1;
hence B1 \/ {x} c= S1 \/ S2 by A26, XBOOLE_1:13; :: thesis: S1 \/ S2 is B,R -derivable
thus S1 \/ S2 is B,R -derivable by A25, A27, Th43; :: thesis: verum

end;

thus S₁[S] from FINSET_1:sch 2(A2, A10, A20); :: thesis: verum