let TG be commutative TopologicalGroup; :: thesis: for U being a_neighborhood of 1_ TG holds element_left_uniformity U = element_right_uniformity U
let U be a_neighborhood of 1_ TG; :: thesis: element_left_uniformity U = element_right_uniformity U

now :: thesis: ( element_left_uniformity U c= element_right_uniformity U & element_right_uniformity U c= element_left_uniformity U )

thus element_left_uniformity U c= element_right_uniformity U :: thesis: element_right_uniformity U c= element_left_uniformity U

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in element_left_uniformity U or x in element_right_uniformity U )
assume x in element_left_uniformity U ; :: thesis: x in element_right_uniformity U
then consider u, v being Element of TG such that
A1: x = [u,v] and
A2: (u ") * v in U ;
v * (u ") in U by A2, GROUP_1:def 12;
hence x in element_right_uniformity U by A1; :: thesis: verum

end;

thus element_right_uniformity U c= element_left_uniformity U :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in element_right_uniformity U or x in element_left_uniformity U )
assume x in element_right_uniformity U ; :: thesis: x in element_left_uniformity U
then consider u, v being Element of TG such that
A3: x = [u,v] and
A4: v * (u ") in U ;
(u ") * v in U by A4, GROUP_1:def 12;
hence x in element_left_uniformity U by A3; :: thesis: verum

end;

end;

hence element_left_uniformity U = element_right_uniformity U ; :: thesis: verum