theorem Th20: :: QC_LANG1:20

for A being QC-alphabet holds
( not VERUM A is atomic & not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal & ( for p being Element of QC-WFF A holds
( not ( p is atomic & p is negative ) & not ( p is atomic & p is conjunctive ) & not ( p is atomic & p is universal ) & not ( p is negative & p is conjunctive ) & not ( p is negative & p is universal ) & not ( p is conjunctive & p is universal ) ) ) )