let p, q be Element of MC-wff ; :: thesis: for X being Subset of MC-wff holds p => (q => (p '&' q)) in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) }
let X be Subset of MC-wff; :: thesis: p => (q => (p '&' q)) in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) }
reconsider pp = [(p => (q => (p '&' q))),5] as Element of [:MC-wff,Proof_Step_Kinds_IPC:] by Th1, ZFMISC_1:87;
set f = <*pp*>;
A1: len <*pp*> = 1 by FINSEQ_1:40;
(<*pp*> . (len <*pp*>)) `1 = p => (q => (p '&' q)) by A1;
then A3: Effect_IPC <*pp*> = p => (q => (p '&' q)) by Def5;
for n being Nat st 1 <= n & n <= len <*pp*> holds
<*pp*>,n is_a_correct_step_wrt_IPC X

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt_IPC X )
assume ( 1 <= n & n <= len <*pp*> ) ; :: thesis: <*pp*>,n is_a_correct_step_wrt_IPC X
then A4: n = 1 by A1, XXREAL_0:1;
A5: (<*pp*> . 1) `2 = 5 ;
(<*pp*> . n) `1 = p => (q => (p '&' q)) by A4;
hence <*pp*>,n is_a_correct_step_wrt_IPC X by A4, A5, Def3; :: thesis: verum

end;

then <*pp*> is_a_proof_wrt_IPC X ;
hence p => (q => (p '&' q)) in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) } by A3; :: thesis: verum