let X be set ; :: thesis: for R being total reflexive Relation of X holds uniformity_induced_by R is axiom_U1
let R be total reflexive Relation of X; :: thesis: uniformity_induced_by R is axiom_U1
rho R is axiom_UP1 by Th21;
hence uniformity_induced_by R is axiom_U1 ; :: thesis: verum