theorem Th27: :: SYSREL:27

for x being object
for R being Relation holds
( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )