let TG be TopologicalGroup; :: thesis: for V being a_neighborhood of 1_ TG holds V " is a_neighborhood of 1_ TG
let V be a_neighborhood of 1_ TG; :: thesis: V " is a_neighborhood of 1_ TG
V " is a_neighborhood of (1_ TG) " by TOPGRP_1:54;
hence V " is a_neighborhood of 1_ TG by GROUP_1:8; :: thesis: verum