for R being non empty reflexive transitive RelStr
for x, y being Element of R st the InternalRel of R reduces x,y holds
[x,y] in the InternalRel of R