let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = p )
}
= Cn X

let X be Subset of (CQC-WFF Al); :: thesis: { p where p is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = p )
}
= Cn X

set PX = { p where p is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = p )
}
;
A1: { p where p is Element of CQC-WFF Al : ex f being FinSequence of 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 Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = p )
}
as Subset of (CQC-WFF Al) by Lm2;
X c= PX by Th29;
then Cn X c= { p where p is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = p )
}
by ;
hence { p where p is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = p ) } = Cn X by A1; :: thesis: verum