let x be set ; :: thesis: for V being RealLinearSpace
for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds
x in A
let V be RealLinearSpace; :: thesis: for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds
x in A
let A be Subset of V; :: thesis: ( x in conv A & (conv A) \ {x} is convex implies x in A )
assume that
A1: x in conv A and
A2: (conv A) \ {x} is convex ; :: thesis: x in A
reconsider A1 = A as non empty Subset of V by A1;
A3: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;
assume A4: not x in A ; :: thesis: contradiction
consider L being Convex_Combination of A1 such that
A5: Sum L = x and
L in ConvexComb V by A1, A3;
set C = Carrier L;
A6: Carrier L c= A1 by RLVECT_2:def 6;
Carrier L <> {} by CONVEX1:21;
then consider p being object such that
A7: p in Carrier L by XBOOLE_0:def 1;
reconsider p = p as Element of V by A7;
A8: sum L = 1 by Th62;
(Carrier L) \ {p} <> {}

proof

assume A9: (Carrier L) \ {p} = {} ; :: thesis: contradiction
then Carrier L = {p} by A7, ZFMISC_1:58;
then A10: L . p = 1 by A8, Th32;
Sum L = (L . p) * p by A7, A9, RLVECT_2:35, ZFMISC_1:58;
then x = p by A5, A10, RLVECT_1:def 8;
hence contradiction by A4, A6, A7; :: thesis: verum

end;

then consider q being object such that
A11: q in (Carrier L) \ {p} by XBOOLE_0:def 1;
reconsider q = q as Element of V by A11;
A12: q in Carrier L by A11, XBOOLE_0:def 5;
then L . q <> 0 by RLVECT_2:19;
then A13: L . q > 0 by Th62;
reconsider mm = min ((L . p),(L . q)) as Real ;
consider Lq being Linear_Combination of {q} such that
A14: Lq . q = mm by RLVECT_4:37;
A15: p <> q by A11, ZFMISC_1:56;
then A16: p - q <> 0. V by RLVECT_1:21;
A17: Carrier Lq c= {q} by RLVECT_2:def 6;
{q} c= A by A6, A12, ZFMISC_1:31;
then Carrier Lq c= A by A17;
then A18: Lq is Linear_Combination of A by RLVECT_2:def 6;
consider Lp being Linear_Combination of {p} such that
A19: Lp . p = mm by RLVECT_4:37;
A20: Carrier Lp c= {p} by RLVECT_2:def 6;
{p} c= A by A6, A7, ZFMISC_1:31;
then Carrier Lp c= A by A20;
then Lp is Linear_Combination of A by RLVECT_2:def 6;
then A21: Lp - Lq is Linear_Combination of A by A18, RLVECT_2:56;
then - (Lp - Lq) is Linear_Combination of A by RLVECT_2:52;
then reconsider Lpq = L + (Lp - Lq), L1pq = L - (Lp - Lq) as Linear_Combination of A1 by A21, RLVECT_2:38;
A22: Sum L1pq = (Sum L) - (Sum (Lp - Lq)) by RLVECT_3:4
.= (Sum L) + (- (Sum (Lp - Lq))) by RLVECT_1:def 11 ;
L . p <> 0 by A7, RLVECT_2:19;
then L . p > 0 by Th62;
then A23: mm > 0 by A13, XXREAL_0:15;
A24: for v being VECTOR of V holds L1pq . v >= 0

proof

let v be VECTOR of V; :: thesis: L1pq . v >= 0
A25: L1pq . v = (L . v) - ((Lp - Lq) . v) by RLVECT_2:54
.= (L . v) - ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;
A26: L . v >= 0 by Th62;

per cases ( v = q or v = p or ( v <> p & v <> q ) ) ;

suppose A27: v = q ; :: thesis: L1pq . v >= 0

then not v in Carrier Lp by A15, A20, TARSKI:def 1;
then Lp . v = 0 ;
hence L1pq . v >= 0 by A23, A14, A25, A26, A27; :: thesis: verum

end;

suppose A28: v = p ; :: thesis: L1pq . v >= 0

L . p >= mm by XXREAL_0:17;
then A29: (L . p) - mm >= mm - mm by XREAL_1:9;
not v in Carrier Lq by A15, A17, A28, TARSKI:def 1;
then Lq . v = 0 ;
hence L1pq . v >= 0 by A19, A25, A28, A29; :: thesis: verum

end;

suppose A30: ( v <> p & v <> q ) ; :: thesis: L1pq . v >= 0

then not v in Carrier Lq by A17, TARSKI:def 1;
then A31: Lq . v = 0 ;
not v in Carrier Lp by A20, A30, TARSKI:def 1;
then Lp . v = 0 ;
hence L1pq . v >= 0 by A25, A31, Th62; :: thesis: verum

end;

end;

end;

Sum (Lp - Lq) = (Sum Lp) - (Sum Lq) by RLVECT_3:4
.= (mm * p) - (Sum Lq) by A19, RLVECT_2:32
.= (mm * p) - (mm * q) by A14, RLVECT_2:32
.= mm * (p - q) by RLVECT_1:34 ;
then A32: Sum (Lp - Lq) <> 0. V by A23, A16, RLVECT_1:11;
A33: sum (Lp - Lq) = (sum Lp) - (sum Lq) by Th36
.= mm - (sum Lq) by A19, A20, Th32
.= mm - mm by A14, A17, Th32
.= 0 ;
A34: for v being VECTOR of V holds Lpq . v >= 0

proof

let v be VECTOR of V; :: thesis: Lpq . v >= 0
A35: Lpq . v = (L . v) + ((Lp - Lq) . v) by RLVECT_2:def 10
.= (L . v) + ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;
A36: L . v >= 0 by Th62;

per cases ( v = p or v = q or ( v <> p & v <> q ) ) ;

suppose A37: v = p ; :: thesis: Lpq . v >= 0

then not v in Carrier Lq by A15, A17, TARSKI:def 1;
then Lpq . v = (L . v) + (mm - 0) by A19, A35, A37;
hence Lpq . v >= 0 by A23, A36; :: thesis: verum

end;

suppose A38: v = q ; :: thesis: Lpq . v >= 0

L . q >= mm by XXREAL_0:17;
then A39: (L . q) - mm >= mm - mm by XREAL_1:9;
not v in Carrier Lp by A15, A20, A38, TARSKI:def 1;
then Lp . v = 0 ;
hence Lpq . v >= 0 by A14, A35, A38, A39; :: thesis: verum

end;

suppose A40: ( v <> p & v <> q ) ; :: thesis: Lpq . v >= 0

then not v in Carrier Lq by A17, TARSKI:def 1;
then A41: Lq . v = 0 ;
not v in Carrier Lp by A20, A40, TARSKI:def 1;
then Lp . v = 0 ;
hence Lpq . v >= 0 by A35, A41, Th62; :: thesis: verum

end;

end;

end;

sum L1pq = (sum L) - (sum (Lp - Lq)) by Th36
.= 1 + 0 by A33, Th62 ;
then A42: L1pq is convex by A24, Th62;
then L1pq in ConvexComb V by CONVEX3:def 1;
then A43: Sum L1pq in conv A1 by A3, A42;
sum Lpq = (sum L) + (sum (Lp - Lq)) by Th34
.= 1 + 0 by A33, Th62 ;
then A44: Lpq is convex by A34, Th62;
then Lpq in ConvexComb V by CONVEX3:def 1;
then A45: Sum Lpq in conv A by A3, A44;
0. V = - (0. V) ;
then - (Sum (Lp - Lq)) <> 0. V by A32;
then Sum L1pq <> x by A5, A22, RLVECT_1:9;
then A46: Sum L1pq in (conv A) \ {x} by A43, ZFMISC_1:56;
Sum Lpq = (Sum L) + (Sum (Lp - Lq)) by RLVECT_3:1;
then Sum Lpq <> x by A5, A32, RLVECT_1:9;
then A47: Sum Lpq in (conv A) \ {x} by A45, ZFMISC_1:56;
((1 / 2) * (Sum Lpq)) + ((1 - (1 / 2)) * (Sum L1pq)) = ((1 / 2) * ((Sum L) + (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by A22, RLVECT_3:1
.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by RLVECT_1:def 5
.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + (((1 / 2) * (Sum L)) + ((1 / 2) * (- (Sum (Lp - Lq))))) by RLVECT_1:def 5
.= ((1 / 2) * (Sum L)) + (((1 / 2) * (Sum (Lp - Lq))) + (((1 / 2) * (- (Sum (Lp - Lq)))) + ((1 / 2) * (Sum L)))) by RLVECT_1:def 3
.= ((1 / 2) * (Sum L)) + ((((1 / 2) * (Sum (Lp - Lq))) + ((1 / 2) * (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def 3
.= ((1 / 2) * (Sum L)) + (((1 / 2) * ((Sum (Lp - Lq)) + (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def 5
.= ((1 / 2) * (Sum L)) + (((1 / 2) * (0. V)) + ((1 / 2) * (Sum L))) by RLVECT_1:5
.= ((1 / 2) * (Sum L)) + ((0. V) + ((1 / 2) * (Sum L)))
.= ((1 / 2) * (Sum L)) + ((1 / 2) * (Sum L))
.= ((1 / 2) + (1 / 2)) * (Sum L) by RLVECT_1:def 6
.= Sum L by RLVECT_1:def 8 ;
then Sum L in (conv A) \ {x} by A2, A46, A47;
hence contradiction by A5, ZFMISC_1:56; :: thesis: verum