forall a: forall b: forall c:
forall Q:a->b:
forall R:b->c:
forall S:a->c:
Q;R&S < (Q&S;R^);(R&Q^ ;S)