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 that
A1: x in U and
A2: U in B2 ; :: thesis: ex V being open Subset of T st
( V in B1 & V c= U )
U is open Subset of T by A2, YELLOW_8:12;
then consider V being Subset of T such that
A3: V in B1 and
A4: V c= U by A1, YELLOW_8:13;
V is open by A3, YELLOW_8:12;
hence ex V being open Subset of T st
( V in B1 & V c= U ) by A3, A4; :: thesis: verum