theorem :: RLAFFIN2:9
for V being RealLinearSpace
for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )