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 and
A2: p in W and
A3: W is open by YELLOW_6:38;
A4: p in A \/ B by A1, A2, XBOOLE_0:def 3;
consider X being Subset of T such that
A5: X = B and
p in X and
A6: X is open by YELLOW_6:38;
W \/ X is open by A3, A6, TOPS_1:37;
hence A \/ B is Element of (OpenNeighborhoods p) by A1, A5, A4, YELLOW_6:39; :: thesis: verum