let X be set ; :: thesis: for R being total transitive Relation of X holds uniformity_induced_by R is axiom_U3
let R be total transitive Relation of X; :: thesis: uniformity_induced_by R is axiom_U3
A1: rho R is axiom_UP3 by Th24;
let S be Element of the entourages of (uniformity_induced_by R); :: according to UNIFORM2:def 11 :: thesis: ex b₁ being Element of the entourages of (uniformity_induced_by R) st b₁ [*] b₁ c= S
reconsider S1 = S as Element of rho R ;
consider W being Element of rho R such that
A2: W * W c= S1 by A1;
thus ex W being Element of the entourages of (uniformity_induced_by R) st W * W c= S by A2; :: thesis: verum