let V be RealLinearSpace; :: 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 r being Real st 0 < r & r < 1 & u in M - N & v in M - N holds

(r * u) + ((1 - r) * v) in M - N

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 r being Real st 0 < r & r < 1 & u in M - N & v in M - N holds

(r * u) + ((1 - r) * v) in M - N

proof

hence
M - N is convex
; :: thesis: verum
let u, v be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & u in M - N & v in M - N holds

(r * u) + ((1 - r) * v) in M - N

let r be Real; :: thesis: ( 0 < r & r < 1 & u in M - N & v in M - N implies (r * u) + ((1 - r) * v) in M - N )

assume that

A2: ( 0 < r & r < 1 ) and

A3: u in M - N and

A4: v in M - N ; :: thesis: (r * u) + ((1 - r) * v) in M - N

v in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A4, RUSUB_5:def 2;

then consider x2, y2 being Element of V such that

A5: v = x2 - y2 and

A6: ( x2 in M & y2 in N ) ;

u in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A3, RUSUB_5:def 2;

then consider x1, y1 being Element of V such that

A7: u = x1 - y1 and

A8: ( x1 in M & y1 in N ) ;

A9: (r * u) + ((1 - r) * v) = ((r * x1) - (r * y1)) + ((1 - r) * (x2 - y2)) by A7, A5, RLVECT_1:34

.= ((r * x1) - (r * y1)) + (((1 - r) * x2) - ((1 - r) * y2)) by RLVECT_1:34

.= (((r * x1) - (r * y1)) + ((1 - r) * x2)) - ((1 - r) * y2) by RLVECT_1:def 3

.= ((r * x1) - ((r * y1) - ((1 - r) * x2))) - ((1 - r) * y2) by RLVECT_1:29

.= ((r * x1) + (((1 - r) * x2) + (- (r * y1)))) - ((1 - r) * y2) by RLVECT_1:33

.= (((r * x1) + ((1 - r) * x2)) + (- (r * y1))) - ((1 - r) * y2) by RLVECT_1:def 3

.= ((r * x1) + ((1 - r) * x2)) + ((- (r * y1)) - ((1 - r) * y2)) by RLVECT_1:def 3

.= ((r * x1) + ((1 - r) * x2)) - ((r * y1) + ((1 - r) * y2)) by RLVECT_1:30 ;

( (r * x1) + ((1 - r) * x2) in M & (r * y1) + ((1 - r) * y2) in N ) by A1, A2, A8, A6;

then (r * u) + ((1 - r) * v) in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A9;

hence (r * u) + ((1 - r) * v) in M - N by RUSUB_5:def 2; :: thesis: verum

end;(r * u) + ((1 - r) * v) in M - N

let r be Real; :: thesis: ( 0 < r & r < 1 & u in M - N & v in M - N implies (r * u) + ((1 - r) * v) in M - N )

assume that

A2: ( 0 < r & r < 1 ) and

A3: u in M - N and

A4: v in M - N ; :: thesis: (r * u) + ((1 - r) * v) in M - N

v in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A4, RUSUB_5:def 2;

then consider x2, y2 being Element of V such that

A5: v = x2 - y2 and

A6: ( x2 in M & y2 in N ) ;

u in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A3, RUSUB_5:def 2;

then consider x1, y1 being Element of V such that

A7: u = x1 - y1 and

A8: ( x1 in M & y1 in N ) ;

A9: (r * u) + ((1 - r) * v) = ((r * x1) - (r * y1)) + ((1 - r) * (x2 - y2)) by A7, A5, RLVECT_1:34

.= ((r * x1) - (r * y1)) + (((1 - r) * x2) - ((1 - r) * y2)) by RLVECT_1:34

.= (((r * x1) - (r * y1)) + ((1 - r) * x2)) - ((1 - r) * y2) by RLVECT_1:def 3

.= ((r * x1) - ((r * y1) - ((1 - r) * x2))) - ((1 - r) * y2) by RLVECT_1:29

.= ((r * x1) + (((1 - r) * x2) + (- (r * y1)))) - ((1 - r) * y2) by RLVECT_1:33

.= (((r * x1) + ((1 - r) * x2)) + (- (r * y1))) - ((1 - r) * y2) by RLVECT_1:def 3

.= ((r * x1) + ((1 - r) * x2)) + ((- (r * y1)) - ((1 - r) * y2)) by RLVECT_1:def 3

.= ((r * x1) + ((1 - r) * x2)) - ((r * y1) + ((1 - r) * y2)) by RLVECT_1:30 ;

( (r * x1) + ((1 - r) * x2) in M & (r * y1) + ((1 - r) * y2) in N ) by A1, A2, A8, A6;

then (r * u) + ((1 - r) * v) in { (x - y) where x, y is Element of V : ( x in M & y in N ) } by A9;

hence (r * u) + ((1 - r) * v) in M - N by RUSUB_5:def 2; :: thesis: verum