for A being QC-alphabet
for F being Element of QC-WFF A holds
( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal )