theorem Th24: :: UNIFORM3:47

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