theorem Th15: :: RLTOPSP1:15

for X being RealLinearSpace
for M, N being Subset of X
for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)