theorem Th15: :: RELSET_1:15
for A, X, Y being set
for R being Relation of X,Y st id A c= R holds
( A c= dom R & A c= rng R )