let T be TopSpace; :: thesis: for B0 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
weight T = card B0
let B0 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
weight T = card B0
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 weight T = card B0 )
assume that
A1: B0 = rng f and
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: weight T = card B0
set M = { (card C) where C is Basis of T : verum } ;
A3: card B0 in { (card C) where C is Basis of T : verum } ;
weight T = meet { (card C) where C is Basis of T : verum } by WAYBEL23:def 5;
hence weight T c= card B0 by A3, SETFAM_1:3; :: according to XBOOLE_0:def 10 :: thesis: card B0 c= weight T
ex B being Basis of T st card B = weight T by WAYBEL23:74;
hence card B0 c= weight T by A1, A2, Th16, CARD_1:11; :: thesis: verum