for T being TopStruct
for b being Basis of T holds weight T c= card b