let T be non empty finite-weight TopSpace; :: thesis: for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
let B be Basis of T; :: thesis: ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
consider B0 being Basis of T, f being Function of the carrier of T, the topology of T such 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 ) ) by Th15;
take B0 ; :: thesis: ( B0 c= B & card B0 = weight T )
thus B0 c= B by A1, A2, Th16; :: thesis: card B0 = weight T
thus card B0 c= weight T by A1, A2, Th17; :: according to XBOOLE_0:def 10 :: thesis: weight T c= card B0
thus weight T c= card B0 by WAYBEL23:73; :: thesis: verum