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