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

then meet F = {} by SETFAM_1:def 1;
hence meet F is convex ; :: thesis: verum

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 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;

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

end;

hence meet F is convex ; :: thesis: verum

end;

end;