theorem :: GOEDCPUC:14

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