let T be TopStruct ; :: thesis: for b being Basis of T holds weight T c= card b
let b be Basis of T; :: thesis: weight T c= card b
card b in { (card B1) where B1 is Basis of T : verum } ;
hence weight T c= card b by SETFAM_1:3; :: thesis: verum