theorem :: CQC_THE2:92

for A being QC-alphabet
for X being Subset of (CQC-WFF A)
for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G