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 ) } ;

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

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

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
;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;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

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