let T be non empty TopSpace; :: thesis: for x, y being Point of T
for B1 being Basis of x
for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let x, y be Point of T; :: thesis: for B1 being Basis of x
for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let B1 be Basis of x; :: thesis: for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let B2 be Basis of y; :: thesis: for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
let U be set ; :: thesis: ( x in U & U in B2 implies ex V being open Subset of T st
( V in B1 & V c= U ) )
assume A1: ( x in U & U in B2 ) ; :: thesis: ex V being open Subset of T st
( V in B1 & V c= U )
then U is open Subset of T by YELLOW_8:21;
then consider V being Subset of T such that
A2: ( V in B1 & V c= U ) by A1, YELLOW_8:22;
V is open by A2, YELLOW_8:21;
hence ex V being open Subset of T st
( V in B1 & V c= U ) by A2; :: thesis: verum