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
per cases ( F = {} or F <> {} ) ;
suppose F = {} ; :: thesis: meet F is convex
end;
suppose A2: F <> {} ; :: thesis: meet F is convex
meet F is convex
proof
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
proof
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 ;
( M is convex & u in M ) by ;
hence (r * u) + ((1 - r) * v) in M by A3, A7; :: thesis: verum
end;
hence (r * u) + ((1 - r) * v) in meet F by ; :: thesis: verum
end;
hence meet F is convex ; :: thesis: verum
end;
end;