theorem :: QC_LANG2:33

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