let T be non empty TopSpace; :: thesis: for p being Point of T
for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
let p be Point of T; :: thesis: for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
let x be Subset of T; :: thesis: ( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )
set Xp = { v where v is Subset of T : ( p in v & v is open ) } ;
reconsider i = x as Subset of T ;
thus ( x in the carrier of (OpenNeighborhoods p) implies ( p in x & x is open ) ) :: thesis: ( p in x & x is open implies x in the carrier of (OpenNeighborhoods p) )

proof

assume x in the carrier of (OpenNeighborhoods p) ; :: thesis: ( p in x & x is open )
then ex v being Subset of T st
( i = v & p in v & v is open ) by Th29;
hence ( p in x & x is open ) ; :: thesis: verum

end;

assume ( p in x & x is open ) ; :: thesis: x in the carrier of (OpenNeighborhoods p)
then x in the carrier of (InclPoset { v where v is Subset of T : ( p in v & v is open ) } ) ;
hence x in the carrier of (OpenNeighborhoods p) by Th3; :: thesis: verum