:: deftheorem defines -Consistent QC_TRANS:def 2 :
for Al, Al2 being QC-alphabet
for P being Subset of (CQC-WFF Al) holds
( P is Al2 -Consistent iff for S being Subset of (CQC-WFF Al2) st P = S holds
S is Consistent );