theorem Th21: :: LOPBAN15:19

for X, Y being RealLinearSpace
for X1 being Subspace of X
for Y1 being Subspace of Y holds [:X1,Y1:] is Subspace of [:X,Y:]