let X be Subset of CQC-WFF; :: thesis: { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } = Cn X
set PX = { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } ;
A1: { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } c= Cn X by Lm12;
reconsider PX = { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } as Subset of CQC-WFF by Lm2;
X c= PX by Th67;
then Cn X c= { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } by Th37, Th68;
hence { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } = Cn X by A1, XBOOLE_0:def 10; :: thesis: verum