theorem Th21: :: UNIFORM3:45

for X being set
for R being total reflexive Relation of X holds rho R is axiom_UP1