let X, Y be TopSpace; for XV being SubSpace of X
for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]
let XV be SubSpace of X; for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]
let YV be SubSpace of Y; [:XV,YV:] is SubSpace of [:X,Y:]
( [:XV,Y:] is SubSpace of [:X,Y:] & [:XV,YV:] is SubSpace of [:XV,Y:] )
by Lm6, Th15;
hence
[:XV,YV:] is SubSpace of [:X,Y:]
by TSEP_1:7; verum