let V be non empty RLSStruct ; :: 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 r being Real st 0 < r & r < 1 & u in {} & v in {} holds
(r * u) + ((1 - r) * v) in {} ;
assume M = {} ; :: thesis: M is convex
hence M is convex by A1, Def2; :: thesis: verum