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

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

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

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

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

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

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