let X be Subset of MC-wff; :: thesis: for p, q, r being Element of MC-wff st X |-_IPC p & X \/ {r} |-_IPC q holds
X \/ {(p => r)} |-_IPC q
let p, q, r be Element of MC-wff ; :: thesis: ( X |-_IPC p & X \/ {r} |-_IPC q implies X \/ {(p => r)} |-_IPC q )
assume A1: ( X |-_IPC p & X \/ {r} |-_IPC q ) ; :: thesis: X \/ {(p => r)} |-_IPC q
X c= X \/ {(p => r)} by XBOOLE_1:7;
then A2: X \/ {(p => r)} |-_IPC p by A1, Th66;
A3: p => r in {(p => r)} by TARSKI:def 1;
{(p => r)} c= X \/ {(p => r)} by XBOOLE_1:7;
then p => r in X \/ {(p => r)} by A3;
then X \/ {(p => r)} |-_IPC p => r by Th67;
then A7: X \/ {(p => r)} |-_IPC r by A2, Th27;
A8: X \/ {r} c= (X \/ {r}) \/ {(p => r)} by XBOOLE_1:7;
(X \/ {r}) \/ {(p => r)} = (X \/ {(p => r)}) \/ {r} by XBOOLE_1:4;
then (X \/ {(p => r)}) \/ {r} |-_IPC q by A1, A8, Th66;
hence X \/ {(p => r)} |-_IPC q by A7, Th116; :: thesis: verum