let B be set ; :: thesis: for R being Rule
for S1, S2 being Formula-finset st S1 is B,R -derivable & S2 is B,R -derivable holds
S1 \/ S2 is B,R -derivable
let R be Rule; :: thesis: for S1, S2 being Formula-finset st S1 is B,R -derivable & S2 is B,R -derivable holds
S1 \/ S2 is B,R -derivable
let S1, S2 be Formula-finset; :: thesis: ( S1 is B,R -derivable & S2 is B,R -derivable implies S1 \/ S2 is B,R -derivable )
assume ( S1 is B,R -derivable & S2 is B,R -derivable ) ; :: thesis: S1 \/ S2 is B,R -derivable
then consider P1, P2 being Formula-sequence such that
A3: P1 is B,R -correct and
A4: S1 = rng P1 and
A5: P2 is B,R -correct and
A6: S2 = rng P2 ;
set P = P1 ^ P2;
reconsider S = rng (P1 ^ P2) as Formula-finset ;
S = S1 \/ S2 by A4, A6, FINSEQ_1:31;
hence S1 \/ S2 is B,R -derivable by A3, A5, Th42; :: thesis: verum