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 ) } = { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. 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 ) } = { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. 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 ) } = { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (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 { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. 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 { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. 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 { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) }
then consider U1 being Subset of X such that
A1: t = x + U1 and
A2: U1 in O and
A3: U1 is a_neighborhood of 0. X ;
U1 in NeighborhoodSystem (0. X) by A3, YELLOW19:2;
hence t in { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } by A1, A2; :: thesis: verum

end;

then A4: { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } c= { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } ;

now :: thesis: for t being object st t in { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } holds
t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) }

let t be object ; :: thesis: ( t in { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } implies t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } )
assume t in { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } ; :: thesis: t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) }
then consider U1 being Subset of X such that
A5: t = x + U1 and
A6: U1 in O and
A7: U1 in NeighborhoodSystem (0. X) ;
U1 is a_neighborhood of 0. X by A7, YELLOW19:2;
hence t in { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } by A5, A6; :: thesis: verum

end;

then { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } c= { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } ;
hence { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } = { (x + U) where U is Subset of X : ( U in O & U in NeighborhoodSystem (0. X) ) } by A4; :: thesis: verum