for T being TopStruct ex b being Basis of T st card b = weight T