for F, G being ZF-formula holds the_argument_of (F => G) = F '&' ('not' G) by Th3;