for S, T being TopSpace st ex K being Basis of S ex L being Basis of T st K = INTERSECTION (L,{([#] S)}) holds
S is SubSpace of T