let T be non empty TopSpace; for x being Point of T
for B being Basis of x
for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
let x be Point of T; for B being Basis of x
for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
let B be Basis of x; for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
let U1, U2 be set ; ( U1 in B & U2 in B implies ex V being open Subset of T st
( V in B & V c= U1 /\ U2 ) )
assume that
A1:
U1 in B
and
A2:
U2 in B
; ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
reconsider U1 = U1, U2 = U2 as open Subset of T by A1, A2, YELLOW_8:12;
A3:
x in U2
by A2, YELLOW_8:12;
x in U1
by A1, YELLOW_8:12;
then
x in U1 /\ U2
by A3, XBOOLE_0:def 4;
then consider V being Subset of T such that
A4:
V in B
and
A5:
V c= U1 /\ U2
by YELLOW_8:13;
V is open
by A4, YELLOW_8:12;
hence
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
by A4, A5; verum