for R being Relation holds
( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) ) by Th15, Th32;