theorem :: QC_LANG2:34

for A being QC-alphabet
for H being Element of QC-WFF A st H is conditional holds
( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )