for E, X, Y being set st E c= [:X,Y:] holds
(.: (pr2 (X,Y))) . E = (pr2 (X,Y)) .: E