let V be RealLinearSpace; :: thesis: for A, B being Subset of V holds Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)
let A, B be Subset of V; :: thesis: Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B)
( Z_Lin (A /\ B) c= Z_Lin A & Z_Lin (A /\ B) c= Z_Lin B ) by Th13, XBOOLE_1:17;
hence Z_Lin (A /\ B) c= (Z_Lin A) /\ (Z_Lin B) by XBOOLE_1:19; :: thesis: verum