theorem :: ZF_LANG:46

for F, H being ZF-formula st H is conditional holds
( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36;