theorem Th17: :: LOPBAN15:15

for X being RealLinearSpace
for Y1, Y2 being Subspace of X holds RLSp2RVSp (Y1 /\ Y2) = (RLSp2RVSp Y1) /\ (RLSp2RVSp Y2)