let T be non empty TopSpace; for p being Point of T
for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
let p be Point of T; for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
let A, B be Element of (OpenNeighborhoods p); A /\ B is Element of (OpenNeighborhoods p)
consider W being Subset of T such that
A1:
W = A
and
A2:
( p in W & W is open )
by YELLOW_6:29;
consider X being Subset of T such that
A3:
X = B
and
A4:
( p in X & X is open )
by YELLOW_6:29;
( p in A /\ B & W /\ X is open )
by A1, A2, A3, A4, XBOOLE_0:def 4;
hence
A /\ B is Element of (OpenNeighborhoods p)
by A1, A3, YELLOW_6:30; verum