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 [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } c= 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 [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } c= Cn X

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { 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 ) } or a in Cn X )

assume a in { 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 ) } ; :: thesis: a in Cn X

then ex q being Element of CQC-WFF Al st

( q = a & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = q ) ) ;

hence a in Cn X by Th28; :: thesis: verum

( f is_a_proof_wrt X & Effect f = p ) } c= 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 [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) } c= Cn X

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { 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 ) } or a in Cn X )

assume a in { 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 ) } ; :: thesis: a in Cn X

then ex q being Element of CQC-WFF Al st

( q = a & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = q ) ) ;

hence a in Cn X by Th28; :: thesis: verum