let T be TopSpace; :: thesis: for B0, B being Basis of T
for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
let B0, B be Basis of T; :: thesis: for f being Function of the carrier of T, the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
let f be Function of the carrier of T, the topology of T; :: thesis: ( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) implies B0 c= B )
assume A1: B0 = rng f ; :: thesis: ( ex x being Point of T st
( x in f . x implies ex U being open Subset of T st
( x in U & not f . x c= U ) ) or B0 c= B )
assume A2: for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ; :: thesis: B0 c= B
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B0 or a in B )
assume A3: a in B0 ; :: thesis: a in B
then reconsider V = a as Subset of T ;
consider b being object such that
A4: b in dom f and
A5: a = f . b by A1, A3, FUNCT_1:def 3;
A6: V is open by A3, YELLOW_8:10;
reconsider b = b as Element of T by A4;
b in V by A2, A5;
then consider U being Subset of T such that
A7: U in B and
A8: b in U and
A9: U c= V by A6, YELLOW_9:31;
U is open by A7, YELLOW_8:10;
then f . b c= U by A2, A8;
hence a in B by A7, A9, XBOOLE_0:def 10, A5; :: thesis: verum