let V be RealLinearSpace; :: thesis: for A being Subset of V holds Affin (conv A) = Affin A
let A be Subset of V; :: thesis: Affin (conv A) = Affin A
thus Affin (conv A) c= Affin A by Th51, Th65; :: according to XBOOLE_0:def 10 :: thesis: Affin A c= Affin (conv A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Affin A or x in Affin (conv A) )
assume x in Affin A ; :: thesis: x in Affin (conv A)
then x in { (Sum L) where L is Linear_Combination of A : sum L = 1 } by Th59;
then consider L being Linear_Combination of A such that
A1: x = Sum L and
A2: sum L = 1 ;
reconsider K = L as Linear_Combination of conv A by Lm1, RLVECT_2:21;
Sum K in { (Sum M) where M is Linear_Combination of conv A : sum M = 1 } by A2;
hence x in Affin (conv A) by A1, Th59; :: thesis: verum