let Y, X be Subset of MC-wff; :: thesis: for p, q, r being Element of MC-wff st X \/ {p} |-_IPC r & Y \/ {q} |-_IPC r holds
(X \/ Y) \/ {(p 'or' q)} |-_IPC r
let p, q, r be Element of MC-wff ; :: thesis: ( X \/ {p} |-_IPC r & Y \/ {q} |-_IPC r implies (X \/ Y) \/ {(p 'or' q)} |-_IPC r )
set U = p 'or' q;
set Z = X \/ Y;
assume A1: ( X \/ {p} |-_IPC r & Y \/ {q} |-_IPC r ) ; :: thesis: (X \/ Y) \/ {(p 'or' q)} |-_IPC r
then A2: X |-_IPC p => r by Th53;
A4: ( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then A5: X \/ Y |-_IPC p => r by A2, Th66;
Y |-_IPC q => r by A1, Th53;
then A6: X \/ Y |-_IPC q => r by A4, Th66;
X \/ Y |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by Th25;
then X \/ Y |-_IPC (q => r) => ((p 'or' q) => r) by A5, Th27;
then A9: X \/ Y |-_IPC (p 'or' q) => r by A6, Th27;
X \/ Y c= (X \/ Y) \/ {(p 'or' q)} by XBOOLE_1:7;
then A11: (X \/ Y) \/ {(p 'or' q)} |-_IPC (p 'or' q) => r by A9, Th66;
{(p 'or' q)} |-_IPC p 'or' q by Th65;
then (X \/ Y) \/ {(p 'or' q)} |-_IPC p 'or' q by Th66, XBOOLE_1:7;
hence (X \/ Y) \/ {(p 'or' q)} |-_IPC r by A11, Th27; :: thesis: verum