5.9.14.

φ(a) . φ(b) . aRb ≝(Ƒ) φ[aRb]