:: deftheorem defines CL SYSREL:def 1 :
for R being Relation holds CL R = R /\ (id (dom R));