let T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum