let B be set ; :: thesis: for R, R1, R2 being Rule holds
( R1 \/ R2 is B,R -derivable iff ( R1 is B,R -derivable & R2 is B,R -derivable ) )
let R, R1, R2 be Rule; :: thesis: ( R1 \/ R2 is B,R -derivable iff ( R1 is B,R -derivable & R2 is B,R -derivable ) )
thus ( R1 \/ R2 is B,R -derivable implies ( R1 is B,R -derivable & R2 is B,R -derivable ) ) :: thesis: ( R1 is B,R -derivable & R2 is B,R -derivable implies R1 \/ R2 is B,R -derivable )

proof

assume A1: R1 \/ R2 is B,R -derivable ; :: thesis: ( R1 is B,R -derivable & R2 is B,R -derivable )
thus R1 is B,R -derivable :: thesis: R2 is B,R -derivable

proof

let S be Formula-finset; :: according to PROOFS_1:def 15 :: thesis: for t being object st [S,t] in R1 holds
B \/ S,R |- t
let t be object ; :: thesis: ( [S,t] in R1 implies B \/ S,R |- t )
assume [S,t] in R1 ; :: thesis: B \/ S,R |- t
then [S,t] in R1 \/ R2 by XBOOLE_0:def 3;
hence B \/ S,R |- t by A1; :: thesis: verum

end;

let S be Formula-finset; :: according to PROOFS_1:def 15 :: thesis: for t being object st [S,t] in R2 holds
B \/ S,R |- t
let t be object ; :: thesis: ( [S,t] in R2 implies B \/ S,R |- t )
assume [S,t] in R2 ; :: thesis: B \/ S,R |- t
then [S,t] in R1 \/ R2 by XBOOLE_0:def 3;
hence B \/ S,R |- t by A1; :: thesis: verum

end;

assume that
A10: R1 is B,R -derivable and
A11: R2 is B,R -derivable ; :: thesis: R1 \/ R2 is B,R -derivable
let S be Formula-finset; :: according to PROOFS_1:def 15 :: thesis: for t being object st [S,t] in R1 \/ R2 holds
B \/ S,R |- t
let t be object ; :: thesis: ( [S,t] in R1 \/ R2 implies B \/ S,R |- t )
assume [S,t] in R1 \/ R2 ; :: thesis: B \/ S,R |- t

per cases then ( [S,t] in R1 or [S,t] in R2 ) by XBOOLE_0:def 3;

suppose [S,t] in R1 ; :: thesis: B \/ S,R |- t

hence B \/ S,R |- t by A10; :: thesis: verum

end;

suppose [S,t] in R2 ; :: thesis: B \/ S,R |- t

hence B \/ S,R |- t by A11; :: thesis: verum

end;

end;