for p, q, r being ZF-formula
for M being non empty set holds M |= (p => q) => ((q => r) => (p => r))