theorem Th1: :: RELAT_1:7

for R being Relation holds R c= [:(dom R),(rng R):]