theorem :: CALCUL_1:32

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds
X |= p