for p, q being ZF-formula holds
( the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q )