theorem Th30:
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;