for T being non empty TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )