let X be Subset of CQC-WFF ; :: thesis: X c= { 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 ) }
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a 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 ) } )
assume A1: a in X ; :: thesis: a 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 ) }
then reconsider p = a as Element of CQC-WFF ;
reconsider pp = [p,0 ] as Element of [:CQC-WFF ,Proof_Step_Kinds :] by Th43, ZFMISC_1:106;
set f = <*pp*>;
A2: ( len <*pp*> = 1 & <*pp*> . 1 = pp ) by FINSEQ_1:57;
then (<*pp*> . (len <*pp*>)) `1 = p by MCART_1:7;
then A3: Effect <*pp*> = p by Def6;
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 ( 1 <= n & n <= len <*pp*> ) ; :: thesis: <*pp*>,n is_a_correct_step_wrt X
then A4: n = 1 by A2, XXREAL_0:1;
then ( (<*pp*> . 1) `2 = 0 & (<*pp*> . n) `1 in X ) by A1, A2, MCART_1:7;
hence <*pp*>,n is_a_correct_step_wrt X by A4, Def4; :: thesis: verum

end;

then <*pp*> is_a_proof_wrt X by Def5;
hence a 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 A3; :: thesis: verum