let X, Y be TopSpace; :: thesis: 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; :: thesis: for YV being SubSpace of Y holds [:XV,YV:] is SubSpace of [:X,Y:]
let YV be SubSpace of Y; :: thesis: [: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; :: thesis: verum