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