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