set X = { V where V is Subset of T : ( p in V & V is open ) } ;
thus OpenNeighborhoods p is transitive ; :: thesis: OpenNeighborhoods p is directed
let x, y be Element of (OpenNeighborhoods p); :: according to YELLOW_6:def 5 :: thesis: ex z being Element of (OpenNeighborhoods p) st
( x <= z & y <= z )
consider V being Subset of T such that
A1: ( x = V & p in V & V is open ) by Th38;
consider W being Subset of T such that
A2: ( y = W & p in W & W is open ) by Th38;
set z = V /\ W;
( p in V /\ W & V /\ W is open ) by A1, A2, TOPS_1:38, XBOOLE_0:def 4;
then V /\ W in { V where V is Subset of T : ( p in V & V is open ) } ;
then reconsider z = V /\ W as Element of (OpenNeighborhoods p) by Th12;
take z ; :: thesis: ( x <= z & y <= z )
( z c= x & z c= y ) by A1, A2, XBOOLE_1:17;
hence ( x <= z & y <= z ) by Th40; :: thesis: verum