let B be set ; :: thesis: for R being Rule
for B1 being set
for a being object st B1,R |- a & ( for b being object st b in B1 holds
B,R |- b ) holds
B,R |- a
let R be Rule; :: thesis: for B1 being set
for a being object st B1,R |- a & ( for b being object st b in B1 holds
B,R |- b ) holds
B,R |- a
let B1 be set ; :: thesis: for a being object st B1,R |- a & ( for b being object st b in B1 holds
B,R |- b ) holds
B,R |- a
let a be object ; :: thesis: ( B1,R |- a & ( for b being object st b in B1 holds
B,R |- b ) implies B,R |- a )
assume that
A1: B1,R |- a and
A2: for b being object st b in B1 holds
B,R |- b ; :: thesis: B,R |- a
consider S being Formula-finset such that
A3: a in S and
A4: S is B1,R -derivable by A1, Th45;
set S1 = B1 /\ S;
for b being object st b in B1 /\ S holds
b in B1 by XBOOLE_0:def 4;
then for b being object st b in B1 /\ S holds
B,R |- b by A2;
then consider S2 being Formula-finset such that
A7: B1 /\ S c= S2 and
A8: S2 is B,R -derivable by Th47;
S is S2,R -derivable by A4, A7, Th48;
then A10: S2 \/ S is B,R -derivable by A8, Th52;
a in S2 \/ S by A3, XBOOLE_0:def 3;
hence B,R |- a by A10; :: thesis: verum