theorem :: SYSREL:30

for x, y being object
for R being Relation holds
( ( R * R = R & R * (R \ (id (dom R))) = {} & [x,y] in R & x <> y implies ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} & [x,y] in R & x <> y implies ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) ) )