for V being RealLinearSpace
for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)