let V be non empty CLSStruct ; :: thesis: for M being Subset of V st M = {} holds
M is convex
let M be Subset of V; :: thesis: ( M = {} implies M is convex )
A1: for u, v being VECTOR of V
for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in {} & v in {} holds
(z * u) + ((1r - z) * v) in {} ;
assume M = {} ; :: thesis: M is convex
hence M is convex by A1, Def23; :: thesis: verum