now

let x, y be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & x in M /\ N & y in M /\ N holds
(r * x) + ((1 - r) * y) in M /\ N
let r be Real; :: thesis: ( 0 < r & r < 1 & x in M /\ N & y in M /\ N implies (r * x) + ((1 - r) * y) in M /\ N )
assume A1: ( 0 < r & r < 1 & x in M /\ N & y in M /\ N ) ; :: thesis: (r * x) + ((1 - r) * y) in M /\ N
then ( x in M & x in N & y in M & y in N ) by XBOOLE_0:def 4;
then ( (r * x) + ((1 - r) * y) in M & (r * x) + ((1 - r) * y) in N ) by A1, Def2;
hence (r * x) + ((1 - r) * y) in M /\ N by XBOOLE_0:def 4; :: thesis: verum

end;

hence for b₁ being Subset of V st b₁ = M /\ N holds
b₁ is convex by Def2; :: thesis: verum