let T be non empty 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 )
( T is finite-weight or T is infinite-weight ) ;
hence ex B1 being Basis of T st
( B1 c= B & card B1 = weight T ) by Lm4, Lm5; :: thesis: verum