let T be non empty TopSpace; for p being Point of
for A, B being Element of holds A \/ B is Element of
let p be Point of ; for A, B being Element of holds A \/ B is Element of
let A, B be Element of ; A \/ B is Element of
consider W being Subset of 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 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
by A1, A5, A4, YELLOW_6:39; verum