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

for I being affinely-independent Subset of V

for B being Subset of V st x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

x in conv (I \ B)

let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V

for B being Subset of V st x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

x in conv (I \ B)

let I be affinely-independent Subset of V; :: thesis: for B being Subset of V st x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

x in conv (I \ B)

let B be Subset of V; :: thesis: ( x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) implies x in conv (I \ B) )

assume that

A1: x in conv I and

A2: for y being set st y in B holds

(x |-- I) . y = 0 ; :: thesis: x in conv (I \ B)

set IB = I \ B;

A3: conv I c= Affin I by Th65;

then x |-- I = x |-- (I \ B) by A1, A2, Th75;

then A4: for v being VECTOR of V st v in I \ B holds

0 <= (x |-- (I \ B)) . v by A1, Th71;

A5: I \ B is affinely-independent by Th43, XBOOLE_1:36;

x in Affin (I \ B) by A1, A2, A3, Th75;

hence x in conv (I \ B) by A4, A5, Th73; :: thesis: verum

for I being affinely-independent Subset of V

for B being Subset of V st x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

x in conv (I \ B)

let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V

for B being Subset of V st x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

x in conv (I \ B)

let I be affinely-independent Subset of V; :: thesis: for B being Subset of V st x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

x in conv (I \ B)

let B be Subset of V; :: thesis: ( x in conv I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) implies x in conv (I \ B) )

assume that

A1: x in conv I and

A2: for y being set st y in B holds

(x |-- I) . y = 0 ; :: thesis: x in conv (I \ B)

set IB = I \ B;

A3: conv I c= Affin I by Th65;

then x |-- I = x |-- (I \ B) by A1, A2, Th75;

then A4: for v being VECTOR of V st v in I \ B holds

0 <= (x |-- (I \ B)) . v by A1, Th71;

A5: I \ B is affinely-independent by Th43, XBOOLE_1:36;

x in Affin (I \ B) by A1, A2, A3, Th75;

hence x in conv (I \ B) by A4, A5, Th73; :: thesis: verum