let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V
for L being Linear_Combination of I st L is convex & Carrier L = I holds
Sum L in Int I
let I be affinely-independent Subset of V; :: thesis: for L being Linear_Combination of I st L is convex & Carrier L = I holds
Sum L in Int I
let L be Linear_Combination of I; :: thesis: ( L is convex & Carrier L = I implies Sum L in Int I )
assume that
A1: L is convex and
A2: Carrier L = I ; :: thesis: Sum L in Int I
reconsider I1 = I as non empty Subset of V by A1, A2, CONVEX1:21;
reconsider K = L as Linear_Combination of I1 ;
K in ConvexComb V by A1, CONVEX3:def 1;
then Sum K in { (Sum M) where M is Convex_Combination of I1 : M in ConvexComb V } by A1;
then A3: Sum K in conv I1 by CONVEX3:5;
A4: ( conv I1 c= Affin I1 & sum L = 1 ) by A1, RLAFFIN1:62, RLAFFIN1:65;
for A being Subset of V st A c< I holds
not Sum K in conv A

proof

let A be Subset of V; :: thesis: ( A c< I implies not Sum K in conv A )
assume A5: A c< I ; :: thesis: not Sum K in conv A
assume A6: Sum K in conv A ; :: thesis: contradiction
( conv A c= Affin A & A c= I ) by A5, RLAFFIN1:65;
then (Sum K) |-- A = (Sum K) |-- I by A6, RLAFFIN1:77
.= K by A3, A4, RLAFFIN1:def 7 ;
then I c= A by A2, RLVECT_2:def 6;
hence contradiction by A5, XBOOLE_0:def 8; :: thesis: verum

end;

hence Sum L in Int I by A3, Def1; :: thesis: verum