let T be non empty TopStruct ; :: thesis: for x being Point of T

for B being Basis of x

for V being Subset of T st V in B holds

( V is open & x in V )

let x be Point of T; :: thesis: for B being Basis of x

for V being Subset of T st V in B holds

( V is open & x in V )

let B be Basis of x; :: thesis: for V being Subset of T st V in B holds

( V is open & x in V )

let V be Subset of T; :: thesis: ( V in B implies ( V is open & x in V ) )

assume A1: V in B ; :: thesis: ( V is open & x in V )

B c= the topology of T by TOPS_2:64;

hence V is open by A1; :: thesis: x in V

x in Intersect B by Def1;

hence x in V by A1, SETFAM_1:43; :: thesis: verum

for B being Basis of x

for V being Subset of T st V in B holds

( V is open & x in V )

let x be Point of T; :: thesis: for B being Basis of x

for V being Subset of T st V in B holds

( V is open & x in V )

let B be Basis of x; :: thesis: for V being Subset of T st V in B holds

( V is open & x in V )

let V be Subset of T; :: thesis: ( V in B implies ( V is open & x in V ) )

assume A1: V in B ; :: thesis: ( V is open & x in V )

B c= the topology of T by TOPS_2:64;

hence V is open by A1; :: thesis: x in V

x in Intersect B by Def1;

hence x in V by A1, SETFAM_1:43; :: thesis: verum