theorem Th12: :: QC_LANG1:12

for A being QC-alphabet
for F being Element of QC-WFF A holds
( ( ((@ F) . 1) `1 = 0 implies F = VERUM A ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )