let Y, X be Subset of MC-wff; :: thesis: for p being Element of MC-wff st X |-_IPC p & X c= Y holds
Y |-_IPC p
let p be Element of MC-wff ; :: thesis: ( X |-_IPC p & X c= Y implies Y |-_IPC p )
assume A1: ( X |-_IPC p & X c= Y ) ; :: thesis: Y |-_IPC p
then p in CnIPC X ;
then ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) by Th16;
then consider g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] such that
L: ( g is_a_proof_wrt_IPC X & Effect_IPC g = p ) ;
( g is_a_proof_wrt_IPC Y & Effect_IPC g = p ) by L, A1, Th10;
then p in CnIPC Y by Th16;
hence Y |-_IPC p ; :: thesis: verum