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 ) } c= Cn X
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { 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 ) } or a in Cn X )
assume a in { 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 ) } ; :: thesis: a in Cn X
then ex q being Element of CQC-WFF st
( q = a & ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = q ) ) ;
hence a in Cn X by Th66; :: thesis: verum