theorem :: ZF_LANG1:35

for H being ZF-formula st H is conditional holds
( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )