theorem :: SYSREL:36

for R being Relation holds
( ( (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} implies ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) ) & ( (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} implies ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) ) )