let x be set ; :: thesis: for V being RealLinearSpace

for A being Subset of V st x in Int A holds

ex L being Linear_Combination of A st

( L is convex & x = Sum L )

let V be RealLinearSpace; :: thesis: for A being Subset of V st x in Int A holds

ex L being Linear_Combination of A st

( L is convex & x = Sum L )

let A be Subset of V; :: thesis: ( x in Int A implies ex L being Linear_Combination of A st

( L is convex & x = Sum L ) )

assume A1: x in Int A ; :: thesis: ex L being Linear_Combination of A st

( L is convex & x = Sum L )

then reconsider A1 = A as non empty Subset of V ;

x in conv A by A1, Def1;

then x in { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

then ex L being Convex_Combination of A1 st

( x = Sum L & L in ConvexComb V ) ;

hence ex L being Linear_Combination of A st

( L is convex & x = Sum L ) ; :: thesis: verum

for A being Subset of V st x in Int A holds

ex L being Linear_Combination of A st

( L is convex & x = Sum L )

let V be RealLinearSpace; :: thesis: for A being Subset of V st x in Int A holds

ex L being Linear_Combination of A st

( L is convex & x = Sum L )

let A be Subset of V; :: thesis: ( x in Int A implies ex L being Linear_Combination of A st

( L is convex & x = Sum L ) )

assume A1: x in Int A ; :: thesis: ex L being Linear_Combination of A st

( L is convex & x = Sum L )

then reconsider A1 = A as non empty Subset of V ;

x in conv A by A1, Def1;

then x in { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

then ex L being Convex_Combination of A1 st

( x = Sum L & L in ConvexComb V ) ;

hence ex L being Linear_Combination of A st

( L is convex & x = Sum L ) ; :: thesis: verum