let Al be QC-alphabet ; for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) holds (All (x,p)) => p 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 ) }
let p be Element of CQC-WFF Al; for x being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) holds (All (x,p)) => p 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 ) }
let x be bound_QC-variable of Al; for X being Subset of (CQC-WFF Al) holds (All (x,p)) => p 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 ) }
let X be Subset of (CQC-WFF Al); (All (x,p)) => p 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 ) }
reconsider pp = [((All (x,p)) => p),6] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;
set f = <*pp*>;
A1:
len <*pp*> = 1
by FINSEQ_1:40;
A2:
<*pp*> . 1 = pp
by FINSEQ_1:40;
then
(<*pp*> . (len <*pp*>)) `1 = (All (x,p)) => p
by A1;
then A3:
Effect <*pp*> = (All (x,p)) => p
by Def6;
for n being Nat st 1 <= n & n <= len <*pp*> holds
<*pp*>,n is_a_correct_step_wrt X
then
<*pp*> is_a_proof_wrt X
;
hence
(All (x,p)) => p 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 A3; verum