theorem Th25: :: UNIFORM3:48

for X being set
for R being total reflexive Relation of X holds uniformity_induced_by R is axiom_U1