theorem Th5: :: EQREL_1:5

for X being set
for x being object
for R being reflexive total Relation of X st x in X holds
[x,x] in R