let X be Subset of CQC-WFF ; :: thesis: VERUM in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) }
reconsider pp = [VERUM ,1] as Element of [:CQC-WFF ,Proof_Step_Kinds :] by Th43, ZFMISC_1:106;
set f = <*pp*>;
A1: len <*pp*> = 1 by FINSEQ_1:57;
A2: <*pp*> . 1 = pp by FINSEQ_1:57;
A3: (<*pp*> . (len <*pp*>)) `1 = VERUM by A1, A2, MCART_1:7;
A4: Effect <*pp*> = VERUM by A3, Def6;
A5: for n being Element of NAT st 1 <= n & n <= len <*pp*> holds
<*pp*>,n is_a_correct_step_wrt X

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X )
assume A6: ( 1 <= n & n <= len <*pp*> ) ; :: thesis: <*pp*>,n is_a_correct_step_wrt X
A7: n = 1 by A1, A6, XXREAL_0:1;
A8: (<*pp*> . 1) `2 = 1 by A2, MCART_1:7;
A9: (<*pp*> . n) `1 = VERUM by A2, A7, MCART_1:7;
thus <*pp*>,n is_a_correct_step_wrt X by A7, A8, A9, Def4; :: thesis: verum

end;

A10: <*pp*> is_a_proof_wrt X by A5, Def5;
thus VERUM in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } by A4, A10; :: thesis: verum