thus
OpenNeighborhoods p is transitive
; OpenNeighborhoods p is directed
let x, y be Element of (OpenNeighborhoods p); YELLOW_6:def 3 ex z being Element of (OpenNeighborhoods p) st
( x <= z & y <= z )
set X = { V where V is Subset of T : ( p in V & V is open ) } ;
consider V being Subset of T such that
A1:
x = V
and
A2:
( p in V & V is open )
by Th29;
consider W being Subset of T such that
A3:
y = W
and
A4:
( p in W & W is open )
by Th29;
set z = V /\ W;
( p in V /\ W & V /\ W is open )
by A2, A4, 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 Th3;
A5:
z c= y
by A3, XBOOLE_1:17;
take
z
; ( x <= z & y <= z )
z c= x
by A1, XBOOLE_1:17;
hence
( x <= z & y <= z )
by A5, Th31; verum