for X being set
for R being reflexive connected total Relation of X
for R2 being Relation of X holds R \, R2 = R