theorem Th28: :: NECKLA_3:28

for R being RelStr
for x being Element of R
for y being set st y in component x holds
[x,y] in EqCl the InternalRel of R