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

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