let T be non empty TopSpace; :: thesis: for p being Point of T
for x being Element of (OpenNeighborhoods p) ex W being Subset of T st
( W = x & p in W & W is open )
let p be Point of T; :: thesis: for x being Element of (OpenNeighborhoods p) ex W being Subset of T st
( W = x & p in W & W is open )
let x be Element of (OpenNeighborhoods p); :: thesis: ex W being Subset of T st
( W = x & p in W & W is open )
set X = { V where V is Subset of T : ( p in V & V is open ) } ;
x in the carrier of ((InclPoset { V where V is Subset of T : ( p in V & V is open ) } ) ~ ) ;
then x in the carrier of (InclPoset { V where V is Subset of T : ( p in V & V is open ) } ) by Th12;
hence ex W being Subset of T st
( W = x & p in W & W is open ) ; :: thesis: verum