theorem Th32: :: CQC_THE1:36

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al holds
( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) )