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 A1: ( U1 in B & U2 in B ) ; :: thesis: ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
then reconsider U1 = U1, U2 = U2 as open Subset of T by YELLOW_8:21;
( x in U1 & x in U2 ) by A1, YELLOW_8:21;
then ( x in U1 /\ U2 & U1 /\ U2 is open ) by TOPS_1:38, XBOOLE_0:def 4;
then consider V being Subset of T such that
A2: ( V in B & V c= U1 /\ U2 ) by YELLOW_8:22;
V is open by A2, YELLOW_8:21;
hence ex V being open Subset of T st
( V in B & V c= U1 /\ U2 ) by A2; :: thesis: verum