theorem :: ZF_LANG:47

for H being ZF-formula st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)