set Xp = { v where v is Subset of T : ( p in v & v is open ) } ;
[#] T in the carrier of (InclPoset { v where v is Subset of T : ( p in v & v is open ) } ) ;
hence not the carrier of (OpenNeighborhoods p) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum