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