for Al being QC-alphabet
for Y, X being Subset of (CQC-WFF Al) st Y = { 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 ) } holds
Y is being_a_theory by Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;