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