theorem :: PREFER_1:17

for X being non empty set
for R being total reflexive Relation of X holds R ~ is total