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

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