theorem :: CQC_THE1:46

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds
q in TAUT Al