for R being Relation holds R /\ [:(dom R),(rng R):] = R by Th1, XBOOLE_1:28;