for X being set
for R being total transitive Relation of X holds rho R is axiom_UP3