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:]
A1: [:XV,Y:] is SubSpace of [:X,Y:] by Lm6;
[:XV,YV:] is SubSpace of [:XV,Y:] by Th17;
hence [:XV,YV:] is SubSpace of [:X,Y:] by A1, TSEP_1:7; :: thesis: verum