theorem :: ZF_LANG1:25

for H being ZF-formula st H is conditional holds
the_antecedent_of H = the_left_argument_of (the_argument_of H)