let V be ComplexLinearSpace; :: thesis: for M, N being Subset of V st M is convex & N is convex holds
M - N is convex
let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies M - N is convex )
assume A1: ( M is convex & N is convex ) ; :: thesis: M - N is convex
for u, v being VECTOR of V
for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M - N & v in M - N holds
(z * u) + ((1r - z) * v) in M - N

proof

let u, v be VECTOR of V; :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M - N & v in M - N holds
(z * u) + ((1r - z) * v) in M - N
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M - N & v in M - N implies (z * u) + ((1r - z) * v) in M - N )
assume A3: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M - N & v in M - N ) ; :: thesis: (z * u) + ((1r - z) * v) in M - N
then consider x1, y1 being Element of V such that
A4: ( u = x1 - y1 & x1 in M & y1 in N ) ;
consider x2, y2 being Element of V such that
A5: ( v = x2 - y2 & x2 in M & y2 in N ) by A3;
A6: ( (z * x1) + ((1r - z) * x2) in M & (z * y1) + ((1r - z) * y2) in N ) by A1, A3, A4, A5, Def202;
(z * u) + ((1r - z) * v) = ((z * x1) - (z * y1)) + ((1r - z) * (x2 - y2)) by A4, A5, CLVECT_1:10
.= ((z * x1) - (z * y1)) + (((1r - z) * x2) - ((1r - z) * y2)) by CLVECT_1:10
.= (((z * x1) - (z * y1)) + ((1r - z) * x2)) - ((1r - z) * y2) by RLVECT_1:def 6
.= ((z * x1) - ((z * y1) - ((1r - z) * x2))) - ((1r - z) * y2) by RLVECT_1:43
.= ((z * x1) + (((1r - z) * x2) + (- (z * y1)))) - ((1r - z) * y2) by RLVECT_1:47
.= (((z * x1) + ((1r - z) * x2)) + (- (z * y1))) - ((1r - z) * y2) by RLVECT_1:def 6
.= ((z * x1) + ((1r - z) * x2)) + ((- (z * y1)) - ((1r - z) * y2)) by RLVECT_1:def 6
.= ((z * x1) + ((1r - z) * x2)) - ((z * y1) + ((1r - z) * y2)) by RLVECT_1:44 ;
hence (z * u) + ((1r - z) * v) in M - N by A6; :: thesis: verum

end;

hence M - N is convex by Def202; :: thesis: verum