let X be LinearTopSpace; :: thesis: for x being Point of X
for O being local_base of X holds { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } is non empty Subset-Family of X
let x be Point of X; :: thesis: for O being local_base of X holds { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } is non empty Subset-Family of X
let O be local_base of X; :: thesis: { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } is non empty Subset-Family of X
set B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } ;
now :: thesis: for t being object st t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds
t in bool the carrier of X
let t be object ; :: thesis: ( t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } implies t in bool the carrier of X )
assume t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } ; :: thesis: t in bool the carrier of X
then consider U1 being Subset of X such that
A1: t = x + U1 and
U1 in O and
U1 is a_neighborhood of 0. X ;
thus t in bool the carrier of X by A1; :: thesis: verum
end;
then { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } c= bool the carrier of X ;
then reconsider B1 = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } as Subset-Family of X ;
A2: [#] X is a_neighborhood of 0. X by TOPGRP_1:21;
consider V being a_neighborhood of 0. X such that
A3: V in O and
V c= [#] X by A2, YELLOW13:def 2;
x + V in B1 by A3;
hence { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } is non empty Subset-Family of X ; :: thesis: verum