now :: thesis: for x, y being VECTOR of V
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 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 that
A1: ( 0 < r & r < 1 ) and
A2: ( x in M /\ N & y in M /\ N ) ; :: thesis: (r * x) + ((1 - r) * y) in M /\ N
( x in N & y in N ) by A2, XBOOLE_0:def 4;
then A3: (r * x) + ((1 - r) * y) in N by A1, Def2;
( x in M & y in M ) by A2, XBOOLE_0:def 4;
then (r * x) + ((1 - r) * y) in M by A1, Def2;
hence (r * x) + ((1 - r) * y) in M /\ N by A3, XBOOLE_0:def 4; :: thesis: verum
end;
hence for b1 being Subset of V st b1 = M /\ N holds
b1 is convex ; :: thesis: verum