let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) holds X c= { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

let X be Subset of (CQC-WFF Al); :: thesis: X c= { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),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 Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

then reconsider p = a as Element of CQC-WFF Al ;

reconsider pp = [p,0] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;

set f = <*pp*>;

A2: len <*pp*> = 1 by FINSEQ_1:40;

A3: <*pp*> . 1 = pp by FINSEQ_1:40;

then (<*pp*> . (len <*pp*>)) `1 = p by A2;

then A4: Effect <*pp*> = p by Def6;

for n being Nat st 1 <= n & n <= len <*pp*> holds

<*pp*>,n is_a_correct_step_wrt X

hence a in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } by A4; :: thesis: verum

( f is_a_proof_wrt X & Effect f = F ) }

let X be Subset of (CQC-WFF Al); :: thesis: X c= { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),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 Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) }

then reconsider p = a as Element of CQC-WFF Al ;

reconsider pp = [p,0] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;

set f = <*pp*>;

A2: len <*pp*> = 1 by FINSEQ_1:40;

A3: <*pp*> . 1 = pp by FINSEQ_1:40;

then (<*pp*> . (len <*pp*>)) `1 = p by A2;

then A4: Effect <*pp*> = p by Def6;

for n being Nat st 1 <= n & n <= len <*pp*> holds

<*pp*>,n is_a_correct_step_wrt X

proof

then
<*pp*> is_a_proof_wrt X
;
let n be 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 A5: n = 1 by A2, XXREAL_0:1;

A6: (<*pp*> . 1) `2 = 0 by A3;

(<*pp*> . n) `1 in X by A1, A3, A5;

hence <*pp*>,n is_a_correct_step_wrt X by A5, A6, Def4; :: thesis: verum

end;assume ( 1 <= n & n <= len <*pp*> ) ; :: thesis: <*pp*>,n is_a_correct_step_wrt X

then A5: n = 1 by A2, XXREAL_0:1;

A6: (<*pp*> . 1) `2 = 0 by A3;

(<*pp*> . n) `1 in X by A1, A3, A5;

hence <*pp*>,n is_a_correct_step_wrt X by A5, A6, Def4; :: thesis: verum

hence a in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } by A4; :: thesis: verum