:: deftheorem defines |= CALCUL_1:def 13 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al holds
( |= p iff {} (CQC-WFF Al) |= p );