theorem :: QC_LANG2:8

for A being QC-alphabet holds
( FALSUM A is negative & the_argument_of (FALSUM A) = VERUM A ) by Th1;