let V be non empty RLSStruct ; :: thesis: for F being Subset-Family of V st ( for M being Subset of V st M in F holds

M is convex ) holds

meet F is convex

let F be Subset-Family of V; :: thesis: ( ( for M being Subset of V st M in F holds

M is convex ) implies meet F is convex )

assume A1: for M being Subset of V st M in F holds

M is convex ; :: thesis: meet F is convex

M is convex ) holds

meet F is convex

let F be Subset-Family of V; :: thesis: ( ( for M being Subset of V st M in F holds

M is convex ) implies meet F is convex )

assume A1: for M being Subset of V st M in F holds

M is convex ; :: thesis: meet F is convex

per cases
( F = {} or F <> {} )
;

end;

suppose A2:
F <> {}
; :: thesis: meet F is convex

meet F is convex

end;proof

hence
meet F is convex
; :: thesis: verum
let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & u in meet F & v in meet F holds

(r * u) + ((1 - r) * v) in meet F

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

assume that

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

A4: u in meet F and

A5: v in meet F ; :: thesis: (r * u) + ((1 - r) * v) in meet F

for M being set st M in F holds

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

end;(r * u) + ((1 - r) * v) in meet F

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

assume that

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

A4: u in meet F and

A5: v in meet F ; :: thesis: (r * u) + ((1 - r) * v) in meet F

for M being set st M in F holds

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

proof

hence
(r * u) + ((1 - r) * v) in meet F
by A2, SETFAM_1:def 1; :: thesis: verum
let M be set ; :: thesis: ( M in F implies (r * u) + ((1 - r) * v) in M )

assume A6: M in F ; :: thesis: (r * u) + ((1 - r) * v) in M

then reconsider M = M as Subset of V ;

A7: v in M by A5, A6, SETFAM_1:def 1;

( M is convex & u in M ) by A1, A4, A6, SETFAM_1:def 1;

hence (r * u) + ((1 - r) * v) in M by A3, A7; :: thesis: verum

end;assume A6: M in F ; :: thesis: (r * u) + ((1 - r) * v) in M

then reconsider M = M as Subset of V ;

A7: v in M by A5, A6, SETFAM_1:def 1;

( M is convex & u in M ) by A1, A4, A6, SETFAM_1:def 1;

hence (r * u) + ((1 - r) * v) in M by A3, A7; :: thesis: verum