theorem :: RELAT_1:8

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