let TG be Abelian TopaddGroup; :: thesis: for U being a_neighborhood of 0_ TG holds element_left_uniformity U = element_right_uniformity U
let U be a_neighborhood of 0_ 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 ex u, v being Element of TG st
( x = [u,v] & (- u) + v in U ) ;
hence x in element_right_uniformity U ; :: 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 ex u, v being Element of TG st
( x = [u,v] & v + (- u) in U ) ;
hence x in element_left_uniformity U ; :: thesis: verum
end;
end;
hence element_left_uniformity U = element_right_uniformity U ; :: thesis: verum