theorem Th31: :: CQC_THE1:35

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds { p where p 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 = p ) } = Cn X