for T being TopSpace
for A being Subset of T
for Bas being Basis of T holds Bas | A is Basis of (T | A)