theorem Th25: :: SYSREL:25

for R being Relation
for x, y being object st [x,y] in CL R holds
( x in dom (CL R) & x = y )