let V be non empty CLSStruct ; :: 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

thus meet F is convex :: thesis: verum

proof

let u, v be VECTOR of V; :: according to CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in meet F & v in meet F holds
(z * u) + ((1r - z) * v) in meet F
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in meet F & v in meet F implies (z * u) + ((1r - z) * v) in meet F )
assume that
A3: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A4: u in meet F and
A5: v in meet F ; :: thesis: (z * u) + ((1r - z) * v) in meet F
for M being set st M in F holds
(z * u) + ((1r - z) * v) in M

proof

let M be set ; :: thesis: ( M in F implies (z * u) + ((1r - z) * v) in M )
assume A6: M in F ; :: thesis: (z * u) + ((1r - z) * 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 (z * u) + ((1r - z) * v) in M by A3, A7; :: thesis: verum

end;

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

end;

end;

end;