let T be non empty TopSpace; :: thesis: 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; :: thesis: for A, B being Element of (OpenNeighborhoods p) holds A /\ B is Element of (OpenNeighborhoods p)
let A, B be Element of (OpenNeighborhoods p); :: thesis: A /\ B is Element of (OpenNeighborhoods p)
consider W being Subset of T such that
A1: ( W = A & p in W & W is open ) by YELLOW_6:38;
consider X being Subset of T such that
A2: ( X = B & p in X & X is open ) by YELLOW_6:38;
A3: p in A /\ B by A1, A2, XBOOLE_0:def 4;
W /\ X is open by A1, A2, TOPS_1:38;
hence A /\ B is Element of (OpenNeighborhoods p) by A1, A2, A3, YELLOW_6:39; :: thesis: verum