let TG be commutative TopologicalGroup; :: thesis: left_uniformity TG = right_uniformity TG
set X = { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;
set Y = { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;
now :: thesis: ( { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } c= { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } & { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } c= { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } )
thus { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } c= { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } :: thesis: { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } c= { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } or x in { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } )
assume x in { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ; :: thesis: x in { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum }
then consider U being a_neighborhood of 1_ TG such that
A1: x = element_left_uniformity U ;
x = element_right_uniformity U by A1, Th12;
hence x in { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ; :: thesis: verum
end;
thus { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } c= { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } or x in { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } )
assume x in { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ; :: thesis: x in { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum }
then consider U being a_neighborhood of 1_ TG such that
A2: x = element_right_uniformity U ;
x = element_left_uniformity U by A2, Th12;
hence x in { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ; :: thesis: verum
end;
end;
then system_left_uniformity TG = system_right_uniformity TG ;
hence left_uniformity TG = right_uniformity TG ; :: thesis: verum