let X be set ; :: thesis: for R being symmetric Relation of X holds uniformity_induced_by R is axiom_U2
let R be symmetric Relation of X; :: thesis: uniformity_induced_by R is axiom_U2
A1: rho R is axiom_UP2 by Th22;
now :: thesis: for S being Element of the entourages of (uniformity_induced_by R) holds S [~] in the entourages of (uniformity_induced_by R)
let S be Element of the entourages of (uniformity_induced_by R); :: thesis: S [~] in the entourages of (uniformity_induced_by R)
reconsider S1 = S as Element of rho R ;
consider T being Element of rho R such that
A2: T c= S1 ~ by A1;
T in rho R ;
then consider S2 being Subset of [:X,X:] such that
A3: T = S2 and
A4: R c= S2 ;
R c= S [~] by A2, A3, A4;
hence S [~] in the entourages of (uniformity_induced_by R) ; :: thesis: verum
end;
hence uniformity_induced_by R is axiom_U2 ; :: thesis: verum