let X be Subset of MC-wff; :: thesis: for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
Effect_IPC f in CnIPC X
let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( f is_a_proof_wrt_IPC X implies Effect_IPC f in CnIPC X )
assume A1: f is_a_proof_wrt_IPC X ; :: thesis: Effect_IPC f in CnIPC X
then A2: 1 <= len f by Th5;
then A3: (f . (len f)) `1 in CnIPC X by A1, Th11;
f <> {} by A2;
hence Effect_IPC f in CnIPC X by A3, Def5; :: thesis: verum