theorem :: RELSET_1:17

for X, Y being set
for R being Relation of X,Y st id Y c= R holds
( Y c= dom R & Y = rng R ) by Th15;