let V be RealLinearSpace; :: thesis: for A being Subset of V holds conv A c= Affin A
let A be Subset of V; :: thesis: conv A c= Affin A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in conv A or x in Affin A )
assume A1: x in conv A ; :: thesis: x in Affin A
then reconsider A1 = A as non empty Subset of V ;
conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;
then consider L being Convex_Combination of A1 such that
A2: Sum L = x and
L in ConvexComb V by A1;
sum L = 1 by Th62;
then x in { (Sum K) where K is Linear_Combination of A : sum K = 1 } by A2;
hence x in Affin A by Th59; :: thesis: verum