theorem Th6: :: ZF_LANG1:6

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