for X, Y being TopSpace
for XV being SubSpace of X
for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]