set SF = { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;
reconsider nG = [#] TG as a_neighborhood of 0_ TG by TOPGRP_1:21;
A1: element_right_uniformity nG in { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;
{ (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } c= bool [: the carrier of TG, the carrier of TG:]
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } or t in bool [: the carrier of TG, the carrier of TG:] )
assume t in { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ; :: thesis: t in bool [: the carrier of TG, the carrier of TG:]
then ex U being a_neighborhood of 0_ TG st t = element_right_uniformity U ;
hence t in bool [: the carrier of TG, the carrier of TG:] ; :: thesis: verum
end;
hence { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:] by A1; :: thesis: verum