let Y, X be Subset of MC-wff; :: thesis: for q, r being Element of MC-wff st X |-_IPC r & Y \/ {r} |-_IPC q holds
X \/ Y |-_IPC q
let q, r be Element of MC-wff ; :: thesis: ( X |-_IPC r & Y \/ {r} |-_IPC q implies X \/ Y |-_IPC q )
assume A1: ( X |-_IPC r & Y \/ {r} |-_IPC q ) ; :: thesis: X \/ Y |-_IPC q
then A2: Y |-_IPC r => q by Th53;
A20: ( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then A3: X \/ Y |-_IPC r => q by A2, Th66;
X \/ Y |-_IPC r by A1, A20, Th66;
hence X \/ Y |-_IPC q by A3, Th27; :: thesis: verum