for T being TopSpace
for B being Basis of T holds B \/ { the carrier of T} is Basis of T