The Mizar article:

Convex Hull, Set of Convex Combinations and Convex Cone

by
Noboru Endou, and
Yasunari Shidama

Received June 16, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: CONVEX3
[ MML identifier index ]


environ

 vocabulary RLVECT_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_1, BOOLE, JORDAN1,
      ARYTM_3, CONVEX1, FINSEQ_4, SEQ_1, CARD_1, RLVECT_2, FUNCT_2, RFINSEQ,
      FINSET_1, CONVEX2, CONVEX3;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
      FINSEQ_1, RELAT_1, FUNCT_1, FINSET_1, CARD_1, NAT_1, STRUCT_0, FUNCT_2,
      RLVECT_1, FINSEQ_4, RLVECT_2, RVSUM_1, CONVEX1, TOPREAL1, RFINSEQ,
      CONVEX2;
 constructors REAL_1, SEQ_1, RUSUB_5, FINSEQ_4, CONVEX1, NAT_1, MONOID_0,
      TOPREAL1, RFINSEQ, MEMBERED;
 clusters RELSET_1, ARYTM_3, STRUCT_0, RLVECT_1, SEQ_1, RUSUB_4, BINARITH,
      XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1, REAL_1,
      XBOOLE_0, REAL_2, AXIOMS, XBOOLE_1, RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4,
      ENUMSET1, CONVEX1, FUNCT_2, NAT_1, TOPREAL1, RFINSEQ, SQUARE_1, CONVEX2,
      RLVECT_3, CARD_2, CARD_4, FINSEQ_5, PARTFUN2, GRAPH_5, RELAT_1, XCMPLX_1;
 schemes BINARITH, RLVECT_4, XBOOLE_0, FINSEQ_1, FUNCT_1;

begin :: Equality of Convex Hull and Set of Convex Combinations

definition let V be RealLinearSpace;
  defpred P[set] means $1 is Convex_Combination of V;
 func ConvexComb(V) -> set means :Def1:
 for L being set holds
  L in it iff L is Convex_Combination of V;
existence
proof
   consider A being set such that
A1: for x being set holds
     x in A iff x in Funcs(the carrier of V, REAL) & P[x] from Separation;
   take A;
   let L be set;
   thus L in A implies L is Convex_Combination of V by A1;
   assume L is Convex_Combination of V;
   hence thesis by A1;
  end;
  uniqueness
  proof
  thus for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
  end;
end;

definition let V be RealLinearSpace, M be non empty Subset of V;
  defpred P[set] means $1 is Convex_Combination of M;
 func ConvexComb(M) -> set means
  for L being set holds
  L in it iff L is Convex_Combination of M;
existence
proof
   consider A being set such that
A1: for x being set holds
     x in A iff x in Funcs(the carrier of V, REAL) & P[x] from Separation;
   take A;
   let L be set;
   thus L in A implies L is Convex_Combination of M by A1;
   assume L is Convex_Combination of M;
   hence thesis by A1;
  end;
  uniqueness
  proof
  thus for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
  end;
end;

theorem Th1:
for V being RealLinearSpace, v being VECTOR of V holds
 ex L being Convex_Combination of V st
  Sum(L) = v &
  (for A being non empty Subset of V st v in A holds
   L is Convex_Combination of A)
proof
   let V be RealLinearSpace;
   let v be VECTOR of V;
   consider L being Linear_Combination of {v} such that
A1:L.v = 1 from LinCEx1;
A2:Carrier(L) c= {v} by RLVECT_2:def 8;
    v in Carrier(L) by A1,RLVECT_2:28;
   then {v} c= Carrier(L) by ZFMISC_1:37;
then A3:{v} = Carrier(L) by A2,XBOOLE_0:def 10;
   consider F being FinSequence of the carrier of V such that
A4:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F)
   by RLVECT_2:def 10;
   deffunc F(set) = L.(F.$1);
   consider f being FinSequence such that
A5:len f = len F &
   for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda;
A6:len F = 1 by A3,A4,FINSEQ_3:105;
   then 1 in Seg len F by FINSEQ_1:4,TARSKI:def 1;
then A7:f.1 = L.(F.1) by A5;

    F = <*v*> by A3,A4,FINSEQ_3:106;
then A8:F.1 = v by FINSEQ_1:def 8;

    rng f c= REAL
   proof
      f = <*1*> by A1,A5,A6,A7,A8,FINSEQ_1:57;
     then rng f = {1} by FINSEQ_1:55;
     hence thesis by ZFMISC_1:37;
   end;
   then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A9:f.1 >= 0 by A1,A7,A8;
    f = <*1*> by A1,A5,A6,A7,A8,FINSEQ_1:57;
then A10:Sum(f) = 1 by RVSUM_1:103;

    for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
   proof
     let n be Nat;
     assume n in dom f;
     then n in Seg len f by FINSEQ_1:def 3;
     hence thesis by A5,A6,A9,FINSEQ_1:4,TARSKI:def 1;
   end;
   then reconsider L as Convex_Combination of V by A4,A5,A10,CONVEX1:def 3;
A11:for A being non empty Subset of V st v in A holds
    L is Convex_Combination of A
   proof
     let A be non empty Subset of V;
     assume v in A;
     then {v} c= A by ZFMISC_1:37;
     hence thesis by A3,RLVECT_2:def 8;
   end;
   take L;
    Sum(L) = 1 * v by A1,A3,RLVECT_2:53;
   hence thesis by A11,RLVECT_1:def 9;
end;

theorem
 for V being RealLinearSpace, v1,v2 being VECTOR of V st v1 <> v2 holds
 ex L being Convex_Combination of V st
  for A being non empty Subset of V st {v1,v2} c= A holds
   L is Convex_Combination of A
proof
   let V be RealLinearSpace;
   let v1,v2 be VECTOR of V;
   assume
A1:v1 <> v2;
   consider L being Linear_Combination of {v1,v2} such that
A2:L.v1 = 1/2 & L.v2 = 1/2 from LinCEx2(A1);
A3:Carrier(L) c= {v1,v2} by RLVECT_2:def 8;
    v1 in Carrier(L) & v2 in Carrier(L) by A2,RLVECT_2:28;
   then {v1,v2} c= Carrier(L) by ZFMISC_1:38;
then A4:{v1,v2} = Carrier(L) by A3,XBOOLE_0:def 10;

   consider F being FinSequence of the carrier of V such that
A5:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F)
   by RLVECT_2:def 10;

   deffunc F(set) = L.(F.$1);
   consider f being FinSequence such that
A6:len f = len F &
   for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda;

A7:len F = 2 by A1,A4,A5,FINSEQ_3:107;
   then 1 in Seg len F & 2 in Seg len F by FINSEQ_1:3;
then A8:f.1 = L.(F.1) & f.2 = L.(F.2) by A6;

    now per cases by A1,A4,A5,FINSEQ_3:108;
     suppose F = <*v1,v2*>;
then A9:  F.1 = v1 & F.2 = v2 by FINSEQ_1:61;
      rng f c= REAL
     proof
        f = <*1/2,1/2*> by A2,A6,A7,A8,A9,FINSEQ_1:61;
       then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9;
       then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:44
            .= {1/2} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A10:  f.1 >= 0 & f.2 >= 0 by A2,A8,A9;
      f = <*1/2,1/2*> by A2,A6,A7,A8,A9,FINSEQ_1:61;
then A11:  Sum(f) = 1/2 + 1/2 by RVSUM_1:107 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A6,A7,A10,FINSEQ_1:4,TARSKI:def 2;
     end;
     then reconsider L as Convex_Combination of V by A5,A6,A11,CONVEX1:def 3;
A12:  for A being non empty Subset of V st {v1,v2} c= A holds
      L is Convex_Combination of A by A4,RLVECT_2:def 8;
     take L;
     thus thesis by A12;

     suppose F = <*v2,v1*>;
then A13:  F.1 = v2 & F.2 = v1 by FINSEQ_1:61;

      rng f c= REAL
     proof
        f = <*1/2,1/2*> by A2,A6,A7,A8,A13,FINSEQ_1:61;
       then f = <*1/2*>^<*1/2*> by FINSEQ_1:def 9;
       then rng f = rng <*1/2*> \/ rng <*1/2*> by FINSEQ_1:44
            .= {1/2} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A14:  f.1 >= 0 & f.2 >= 0 by A2,A8,A13;
      f = <*1/2,1/2*> by A2,A6,A7,A8,A13,FINSEQ_1:61;
then A15:  Sum(f) = 1/2 + 1/2 by RVSUM_1:107 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A6,A7,A14,FINSEQ_1:4,TARSKI:def 2;
     end;
     then reconsider L as Convex_Combination of V by A5,A6,A15,CONVEX1:def 3;
A16:  for A being non empty Subset of V st {v1,v2} c= A holds
      L is Convex_Combination of A by A4,RLVECT_2:def 8;
     take L;
     thus thesis by A16;
   end;
   hence thesis;
end;

theorem
 for V being RealLinearSpace, v1,v2,v3 being VECTOR of V
 st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
  ex L being Convex_Combination of V st
   for A being non empty Subset of V st {v1,v2,v3} c= A holds
    L is Convex_Combination of A
proof
   let V be RealLinearSpace;
   let v1,v2,v3 be VECTOR of V;
   assume that
A1:v1 <> v2 and
A2:v1 <> v3 and
A3:v2 <> v3;
   consider L being Linear_Combination of {v1,v2,v3} such that
A4:L.v1 = 1/3 & L.v2 = 1/3 & L.v3 = 1/3 from LinCEx3(A1,A2,A3);
A5:Carrier(L) c= {v1,v2,v3} by RLVECT_2:def 8;
    for x being set st x in {v1,v2,v3} holds x in Carrier(L)
   proof
     let x be set;
     assume A6:x in {v1,v2,v3};
     then reconsider x as VECTOR of V;
      x = v1 or x = v2 or x = v3 by A6,ENUMSET1:13;
     hence thesis by A4,RLVECT_2:28;
   end;
   then {v1,v2,v3} c= Carrier(L) by TARSKI:def 3;
then A7:{v1,v2,v3} = Carrier(L) by A5,XBOOLE_0:def 10;

   consider F being FinSequence of the carrier of V such that
A8:F is one-to-one & rng F = Carrier(L) & Sum(L) = Sum(L (#) F)
   by RLVECT_2:def 10;

   deffunc F(set) = L.(F.$1);
   consider f being FinSequence such that
A9:len f = len F &
   for n being Nat st n in Seg(len F) holds f.n = F(n) from SeqLambda;

A10:len F = 3 by A1,A2,A3,A7,A8,FINSEQ_3:110;
   then 1 in Seg len F & 2 in Seg len F & 3 in Seg len F by FINSEQ_1:3;
then A11:f.1 = L.(F.1) & f.2 = L.(F.2) & f.3 = L.(F.3) by A9;

    now per cases by A1,A2,A3,A7,A8,CONVEX1:31;
     suppose F = <*v1,v2,v3*>;
then A12:  F.1 = v1 & F.2 = v2 & F.3 = v3 by FINSEQ_1:62;

      rng f c= REAL
     proof
        f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A12,FINSEQ_1:62;
       then f = <*1/3*>^<*1/3*>^<*1/3*> by FINSEQ_1:def 10;
       then rng f = rng (<*1/3*>^<*1/3*>) \/ rng <*1/3*> by FINSEQ_1:44
            .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
            .= {1/3} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A13:  f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A12;
      f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A12,FINSEQ_1:62;
then A14:  Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A9,A10,A13,ENUMSET1:13,FINSEQ_3:1;
     end;
     then reconsider L as Convex_Combination of V by A8,A9,A14,CONVEX1:def 3;
A15:  for A being non empty Subset of V st {v1,v2,v3} c= A holds
      L is Convex_Combination of A by A7,RLVECT_2:def 8;
     take L;
     thus thesis by A15;

     suppose F = <* v1,v3,v2*>;
then A16:  F.1 = v1 & F.2 = v3 & F.3 = v2 by FINSEQ_1:62;

      rng f c= REAL
     proof
        f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A16,FINSEQ_1:62;
       then f = <*1/3*>^<*1/3*>^<*1/3*> by FINSEQ_1:def 10;
       then rng f = rng (<*1/3*>^<*1/3*>) \/ rng <*1/3*> by FINSEQ_1:44
            .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
            .= {1/3} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A17:  f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A16;
      f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A16,FINSEQ_1:62;
then A18:  Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A9,A10,A17,ENUMSET1:13,FINSEQ_3:1;
     end;
     then reconsider L as Convex_Combination of V by A8,A9,A18,CONVEX1:def 3;
A19:  for A being non empty Subset of V st {v1,v2,v3} c= A holds
      L is Convex_Combination of A by A7,RLVECT_2:def 8;
     take L;
     thus thesis by A19;

     suppose F = <*v2,v1,v3*>;
then A20:  F.1 = v2 & F.2 = v1 & F.3 = v3 by FINSEQ_1:62;

      rng f c= REAL
     proof
        f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A20,FINSEQ_1:62;
       then f = <*1/3*>^<*1/3*>^<*1/3*> by FINSEQ_1:def 10;
       then rng f = rng (<*1/3*>^<*1/3*>) \/ rng <*1/3*> by FINSEQ_1:44
            .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
            .= {1/3} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A21:  f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A20;
      f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A20,FINSEQ_1:62;
then A22:  Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A9,A10,A21,ENUMSET1:13,FINSEQ_3:1;
     end;
     then reconsider L as Convex_Combination of V by A8,A9,A22,CONVEX1:def 3;
A23:  for A being non empty Subset of V st {v1,v2,v3} c= A holds
      L is Convex_Combination of A by A7,RLVECT_2:def 8;
     take L;
     thus thesis by A23;

     suppose F = <* v2,v3,v1*>;
then A24:  F.1 = v2 & F.2 = v3 & F.3 = v1 by FINSEQ_1:62;

      rng f c= REAL
     proof
        f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A24,FINSEQ_1:62;
       then f = <*1/3*>^<*1/3*>^<*1/3*> by FINSEQ_1:def 10;
       then rng f = rng (<*1/3*>^<*1/3*>) \/ rng <*1/3*> by FINSEQ_1:44
            .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
            .= {1/3} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A25:  f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A24;
      f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A24,FINSEQ_1:62;
then A26:  Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A9,A10,A25,ENUMSET1:13,FINSEQ_3:1;
     end;
     then reconsider L as Convex_Combination of V by A8,A9,A26,CONVEX1:def 3;
A27:  for A being non empty Subset of V st {v1,v2,v3} c= A holds
      L is Convex_Combination of A by A7,RLVECT_2:def 8;
     take L;
     thus thesis by A27;

     suppose F = <* v3,v1,v2*>;
then A28:  F.1 = v3 & F.2 = v1 & F.3 = v2 by FINSEQ_1:62;

      rng f c= REAL
     proof
        f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A28,FINSEQ_1:62;
       then f = <*1/3*>^<*1/3*>^<*1/3*> by FINSEQ_1:def 10;
       then rng f = rng (<*1/3*>^<*1/3*>) \/ rng <*1/3*> by FINSEQ_1:44
            .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
            .= {1/3} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A29:  f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A28;
      f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A28,FINSEQ_1:62;
then A30:  Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;

      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A9,A10,A29,ENUMSET1:13,FINSEQ_3:1;
     end;
     then reconsider L as Convex_Combination of V by A8,A9,A30,CONVEX1:def 3;
A31:  for A being non empty Subset of V st {v1,v2,v3} c= A holds
      L is Convex_Combination of A by A7,RLVECT_2:def 8;
     take L;
     thus thesis by A31;

     suppose F = <* v3,v2,v1*>;
then A32:  F.1 = v3 & F.2 = v2 & F.3 = v1 by FINSEQ_1:62;

      rng f c= REAL
     proof
        f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A32,FINSEQ_1:62;
       then f = <*1/3*>^<*1/3*>^<*1/3*> by FINSEQ_1:def 10;
       then rng f = rng (<*1/3*>^<*1/3*>) \/ rng <*1/3*> by FINSEQ_1:44
            .= rng <*1/3*> \/ rng <*1/3*> \/ rng <*1/3*> by FINSEQ_1:44
            .= {1/3} by FINSEQ_1:55;
       hence thesis by ZFMISC_1:37;
     end;
     then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

A33:  f.1 >= 0 & f.2 >= 0 & f.3 >= 0 by A4,A11,A32;
      f = <*1/3,1/3,1/3*> by A4,A9,A10,A11,A32,FINSEQ_1:62;
then A34:  Sum(f) = 1/3 + 1/3 + 1/3 by RVSUM_1:108 .= 1;
      for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume n in dom f;
       then n in Seg len f by FINSEQ_1:def 3;
       hence thesis by A9,A10,A33,ENUMSET1:13,FINSEQ_3:1;
     end;
     then reconsider L as Convex_Combination of V by A8,A9,A34,CONVEX1:def 3;
A35:  for A being non empty Subset of V st {v1,v2,v3} c= A holds
      L is Convex_Combination of A by A7,RLVECT_2:def 8;
     take L;
     thus thesis by A35;
   end;
   hence thesis;
end;

Lm1:
for V being RealLinearSpace, M being non empty Subset of V st
 {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M holds
  M is convex
proof
   let V be RealLinearSpace;
   let M be non empty Subset of V;
   assume
A1:{Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M;
    for u,v being VECTOR of V, r being Real st
   0 < r & r < 1 & u in M & v in M holds r*u + (1-r)*v in M
   proof
     let u,v be VECTOR of V;
     let r be Real;
     set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
     assume
A2:  0 < r & r < 1 & u in M & v in M;
     consider Lu being Convex_Combination of V such that
A3:  Sum(Lu) = u &
      (for A being non empty Subset of V st u in A holds
       Lu is Convex_Combination of A) by Th1;
     reconsider Lu as Convex_Combination of M by A2,A3;

     consider Lv being Convex_Combination of V such that
A4:  Sum(Lv) = v &
      (for A being non empty Subset of V st v in A holds
       Lv is Convex_Combination of A) by Th1;
     reconsider Lv as Convex_Combination of M by A2,A4;
A5:  r*u + (1-r)*v = Sum(r*Lu) + (1-r)*Sum(Lv) by A3,A4,RLVECT_3:2
       .= Sum(r*Lu) + Sum((1-r)*Lv) by RLVECT_3:2
       .= Sum(r*Lu + (1-r)*Lv) by RLVECT_3:1;
A6:  r*Lu + (1-r)*Lv is Convex_Combination of M by A2,CONVEX2:10;
     then r*Lu + (1-r)*Lv in ConvexComb(V) by Def1;
     then r*u + (1-r)*v in S by A5,A6;
     hence thesis by A1;
   end;
   hence thesis by CONVEX1:def 2;
end;

Lm2:
for V being RealLinearSpace, M being non empty Subset of V,
 L being Convex_Combination of M st card Carrier(L) >= 2 holds
  ex L1,L2 being Convex_Combination of M, r being Real st
   0 < r & r < 1 & L = r*L1 + (1-r)*L2 & card Carrier(L1) = 1 &
    card Carrier(L2) = card Carrier(L) - 1
proof
   let V be RealLinearSpace;
   let M be non empty Subset of V;
   let L be Convex_Combination of M;
   assume
A1:card Carrier(L) >= 2;

   consider F being FinSequence of the carrier of V such that
A2:F is one-to-one & rng F = Carrier L &
    (ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 &
     (for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0))
      by CONVEX1:def 3;

   consider f being FinSequence of REAL such that
A3: len f = len F & Sum(f) = 1 &
     (for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0) by A2;

   A4: for n,m being Nat st 1 <= n & n < m & m <= len F holds F.n <> F.m
   proof
     let n,m be Nat;
     assume
A5:  1 <= n & n < m & m <= len F;
     assume
A6:  F.n = F.m;
      n <= len F & 1 <= m by A5,AXIOMS:22;
     then n in Seg len F & m in Seg len F by A5,FINSEQ_1:3;
     then n in dom F & m in dom F by FINSEQ_1:def 3;
     hence contradiction by A2,A5,A6,FUNCT_1:def 8;
   end;
then A7:len F >= 2 by A1,A2,GRAPH_5:10;
    len F >= 1 + 1 by A1,A2,A4,GRAPH_5:10;
then A8:len F - 1 >= 1 by REAL_1:84;
    len F <> 0 by A7;
   then consider i being Nat such that
A9:len F = i + 1 by NAT_1:22;
A10:len F - 1 = i by A9,XCMPLX_1:26;
   set v = F.len F;
    1 <= len F by A7,AXIOMS:22;
then A11:len F in dom F by FINSEQ_3:27;
then A12:F.(len F) in rng F & rng F c= the carrier of V by FINSEQ_1:def 4,
FUNCT_1:12;
   then reconsider v as VECTOR of V;
   consider L1 being Convex_Combination of V such that
A13:Sum(L1) = v &
   (for A being non empty Subset of V st v in A holds
    L1 is Convex_Combination of A) by Th1;

A14:v in Carrier L & Carrier L c= M
     by A2,A11,FUNCT_1:12,RLVECT_2:def 8;
   then reconsider L1 as Convex_Combination of M by A13;

    1 <= len f by A3,A7,AXIOMS:22;
   then len f in Seg len f by FINSEQ_1:3;
then A15:len f in dom f by FINSEQ_1:def 3;
   then f.(len f) in rng f & rng f c= REAL by FINSEQ_1:def 4,FUNCT_1:12;
   then reconsider r = f.len f as Real;

A16:0 < r & r < 1
   proof
A17:  f.(len f) = L.(F.(len f)) & f.(len f) >= 0 by A3,A15;
      F.(len F) in rng F by A11,FUNCT_1:12;
then A18:  r <> 0 & r >= 0 by A2,A3,A17,RLVECT_2:28;
A19:  f = (f|i)^(f/^i) by RFINSEQ:21;
      f/^i = <*f/.(len f)*> by A3,A9,FINSEQ_5:33
         .= <*f.(len f)*> by A15,FINSEQ_4:def 4;
     then Sum(f) = Sum(f|i) + r by A19,RVSUM_1:104;
then A20:  Sum(f|i) = 1 - r by A3,XCMPLX_1:26;
      Sum(f|i) > 0
     proof
A21:   for k being Nat st k in dom(f|i) holds 0 <= (f|i).k
       proof
         let k be Nat;
         assume
A22:      k in dom(f|i);
          f|i = f|Seg i by TOPREAL1:def 1;
then A23:      (f|i).k = f.k by A22,FUNCT_1:68;
          dom(f|i) c= dom f by FINSEQ_5:20;
         hence thesis by A3,A22,A23;
       end;

        ex k being Nat st k in dom(f|i) & 0 < (f|i).k
       proof
A24:      1 in Seg i by A8,A10,FINSEQ_1:3;
          1 <= len f by A3,A7,AXIOMS:22;
then A25:     1 in Seg len f by FINSEQ_1:3;
then A26:      1 in dom f by FINSEQ_1:def 3;
then A27:    1 in dom(f|(Seg i)) by A24,RELAT_1:86;
then A28:     1 in dom(f|i) by TOPREAL1:def 1;
          f|i = f|Seg i by TOPREAL1:def 1;
then A29:     (f|i).1 = f.1 by A27,FUNCT_1:68
          .= L.(F.1) by A3,A26;
          1 in dom F by A3,A25,FINSEQ_1:def 3;
         then F.1 in rng F by FUNCT_1:12;
then A30:     L.(F.1) <> 0 by A2,RLVECT_2:28;
          (f|i).1 >= 0 by A21,A28;
         hence thesis by A28,A29,A30;
       end;
       hence thesis by A21,RVSUM_1:115;
     end;
     then 1 > r + 0 by A20,REAL_1:86;
     hence thesis by A18;
   end;

   set r' = 1/(1 - r);

    1 > r + 0 by A16;
then A31:1 - r > 0 by REAL_1:86;
then A32:r' > 0 by REAL_2:127;

   defpred P[set,set] means
    ($1 in (rng F \ {v}) implies $2 = r'*(L.$1)) &
    (not ($1 in (rng F \ {v})) implies $2 = 0);
A33:for x,y1,y2 being set st
    x in the carrier of V & P[x,y1] & P[x,y2]
    holds y1 = y2;

A34:for x being set st x in the carrier of V
    ex y being set st P[x,y]
   proof
     let x be set;
     assume x in the carrier of V;
      x in (rng F \ {v}) or not (x in (rng F \ {v}));
     hence thesis;
   end;

   consider L2 being Function such that
A35:dom L2 = the carrier of V &
   for x being set st x in the carrier of V holds P[x,L2.x]
    from FuncEx(A33,A34);

    for y being set st y in rng L2 holds y in REAL
   proof
     let y be set;
     assume y in rng L2;
     then consider x being set such that
A36: x in dom L2 & y = L2.x by FUNCT_1:def 5;
      now per cases;
       suppose
A37:    x in (rng F \ {v});
       then x in rng F by XBOOLE_0:def 4;
       then reconsider x as VECTOR of V by A2;
        y = r'*L.x by A35,A36,A37 .= (r'*L).x by RLVECT_2:def 13;
       hence thesis;

       suppose not (x in (rng F \ {v}));
       then y = 0 by A35,A36;
       hence thesis;
     end;
     hence thesis;
   end;
   then rng L2 c= REAL by TARSKI:def 3;
then A38:L2 is Element of Funcs(the carrier of V, REAL) by A35,FUNCT_2:def 2;
    ex T being finite Subset of V st
    for v being Element of V st not v in T holds L2.v = 0
   proof
     reconsider T = Carrier(L) \ {v} as finite Subset of V;
     take T;
     thus thesis by A2,A35;
   end;
   then reconsider L2 as Linear_Combination of V by A38,RLVECT_2:def 5;

    for n,m being Nat st
    n in dom (F|i) & m in dom (F|i) & (F|i)/.n = (F|i)/.m holds n = m
   proof
     let n,m be Nat;
     assume that
A39: n in dom(F|i) and
A40: m in dom(F|i) and
A41: (F|i)/.n = (F|i)/.m;
A42: dom(F|i) c= dom F by FINSEQ_5:20;
      F/.n = (F|i)/.n by A39,TOPREAL1:1 .= F/.m by A40,A41,TOPREAL1:1;
     hence thesis by A2,A39,A40,A42,PARTFUN2:17;
   end;
then A43:F|i is one-to-one by PARTFUN2:16;

A44:Carrier(L2) = Carrier(L) \ {v}
   proof
      for u being set st u in Carrier(L2) holds u in Carrier(L) \ {v}
     proof
       let u be set;
       assume
A45:   u in Carrier(L2);
       then reconsider u as Element of V;
        L2.u <> 0 by A45,RLVECT_2:28;
       hence thesis by A2,A35;
     end;
then A46: Carrier(L2) c= Carrier(L) \ {v} by TARSKI:def 3;

      for u being set st u in Carrier(L) \ {v} holds u in Carrier(L2)
     proof
       let u be set;
       assume
A47:   u in Carrier(L) \ {v};
       then reconsider u as Element of V;
A48:   u in Carrier(L) by A47,XBOOLE_0:def 4;
A49:   L2.u = r'*L.u by A2,A35,A47;
        L.u <> 0 by A48,RLVECT_2:28;
       then L2.u <> 0 by A32,A49,XCMPLX_1:6;
       hence thesis by RLVECT_2:28;
     end;
     then Carrier(L) \ {v} c= Carrier(L2) by TARSKI:def 3;
     hence thesis by A46,XBOOLE_0:def 10;
   end;
   then Carrier(L2) c= Carrier(L) & Carrier(L) c= M
     by RLVECT_2:def 8,XBOOLE_1:36;
   then Carrier(L2) c= M by XBOOLE_1:1;
   then reconsider L2 as Linear_Combination of M by RLVECT_2:def 8;

A50:rng(F|i) = Carrier(L2)
   proof
      F = (F|i)^(F/^i) by RFINSEQ:21;
then A51: Carrier(L) = rng(F|i) \/ rng(F/^i) by A2,FINSEQ_1:44;
      rng(F|i) misses rng(F/^i) by A2,FINSEQ_5:37;
then A52: Carrier(L) \ rng(F/^i) = rng(F|i) by A51,XBOOLE_1:88;
      F/^i = <*F/.(len F)*> by A9,FINSEQ_5:33
         .= <*F.(len F)*> by A11,FINSEQ_4:def 4;
     hence thesis by A44,A52,FINSEQ_1:55;
   end;

   deffunc F(set) = L2.((F|i).$1);
   consider f2 being FinSequence such that
A53:len f2 = len(F|i) &
   for k being Nat st k in Seg len(F|i) holds f2.k = F(k) from SeqLambda;

    for y being set st y in rng f2 holds y in REAL
   proof
     let y be set;
     assume y in rng f2;
     then consider x being set such that
A54: x in dom f2 & y = f2.x by FUNCT_1:def 5;
A55: x in Seg len f2 by A54,FINSEQ_1:def 3;
     then reconsider x as Nat;
      x in dom (F|i) by A53,A55,FINSEQ_1:def 3;
then A56: (F|i).x in rng (F|i) by FUNCT_1:12;
     consider L2' being Function such that
A57: L2 = L2' & dom L2' = the carrier of V & rng L2' c= REAL by FUNCT_2:def 2;
      L2.((F|i).x) in rng L2 by A50,A56,A57,FUNCT_1:12;
     then L2.((F|i).x) in REAL by A57;
     hence thesis by A53,A54,A55;
   end;
   then rng f2 c= REAL by TARSKI:def 3;
   then reconsider f2 as FinSequence of REAL by FINSEQ_1:def 4;

Sum(f2) = 1 &
   (for n being Nat st n in dom(f2) holds f2.n = L2.((F|i).n) & f2.n >= 0)
   proof
A58:  i <= len F by A9,NAT_1:37;
A59:  dom f2 = Seg len (F|i) by A53,FINSEQ_1:def 3;
then A60:  dom f2 = Seg i by A58,TOPREAL1:3
           .= Seg len (f|i) by A3,A58,TOPREAL1:3
           .= dom (f|i) by FINSEQ_1:def 3;
then A61: dom f2 = dom (r'*(f|i)) by RVSUM_1:65;
A62:  for k being Nat st k in dom f2 holds f2.k = (r'*(f|i)).k & f2.k >= 0
     proof
       let k be Nat;
       assume
A63:    k in dom f2;
then A64:    f2.k = L2.((F|i).k) by A53,A59;
        k in dom (f|Seg i) & f|i = f|(Seg i) by A60,A63,TOPREAL1:def 1;
then A65:    k in dom f /\ Seg i & (f|i).k = f.k
         by FUNCT_1:68;
then A66:   k in dom f by XBOOLE_0:def 3;
then A67:    (f|i).k = L.(F.k) by A3,A65;
A68:   k in dom (F|i) by A59,A63,FINSEQ_1:def 3;
A69:   F|i = F|Seg i by TOPREAL1:def 1;
then A70:   (F|i).k = F.k by A68,FUNCT_1:68;
A71:   (f|i).k = L.((F|i).k) by A67,A68,A69,FUNCT_1:68;
        (F|i).k in rng(F|i) by A68,FUNCT_1:12;
       then reconsider w = (F|i).k as Element of V by A50;

A72:   not w in {v}
       proof
         assume w in {v};
then A73:     F.k = v by A70,TARSKI:def 1;
          dom (F|Seg i) c= dom F by FUNCT_1:76;
then A74:     k = len F by A2,A11,A68,A69,A73,FUNCT_1:def 8;
          k <= len(F|i) & len(F|i) <= i by A59,A63,FINSEQ_1:3,FINSEQ_5:19;
         then k <= i by AXIOMS:22;
         then k + 1 <= len F by A10,REAL_1:84;
         hence contradiction by A74,NAT_1:38;
       end;

        now per cases;
         suppose w in (rng F \ {v});
then A75:     L2.w = r'*(L.w) by A35
             .= r'*(f|i).k by A67,A68,A69,FUNCT_1:68
             .= (r'*(f|i)).k by RVSUM_1:66;
          f.k >= 0 by A3,A66;
         then r'*(f|i).k >= 0 by A32,A65,SQUARE_1:19;
         hence thesis by A64,A75,RVSUM_1:66;

         suppose
A76:     not w in (rng F \ {v});
then A77:     not w in rng F by A72,XBOOLE_0:def 4;
A78:     f2.k = 0 by A35,A64,A76;
          L.w = 0 by A2,A77,RLVECT_2:28;
         then r'*(f|i).k = 0 by A71;
         hence thesis by A78,RVSUM_1:66;
       end;
       hence thesis;
     end;
     then for k being Nat st k in dom f2 holds f2.k = (r'*(f|i)).k;
then A79:  f2 = r'*(f|i) by A61,FINSEQ_1:17;

A80:  f = (f|i)^(f/^i) by RFINSEQ:21;
      f/^i = <*f/.(len f)*> by A3,A9,FINSEQ_5:33
         .= <*f.(len f)*> by A15,FINSEQ_4:def 4;
     then Sum(f) = Sum(f|i) + r by A80,RVSUM_1:104;
     then Sum(f|i) = 1 - r by A3,XCMPLX_1:26;
     hence Sum(f2) = 1/(1-r)*(1-r) by A79,RVSUM_1:117
            .= 1/((1-r)/(1-r)) by XCMPLX_1:82
            .= 1/1 by A31,XCMPLX_1:60
            .= 1;
     thus thesis by A53,A59,A62;
   end;
   then reconsider L2 as Convex_Combination of M by A43,A50,A53,CONVEX1:def 3;
A81:v in {v} by TARSKI:def 1;
   reconsider B = {v} as non empty Subset of V by TARSKI:def 1;
    L1 is Convex_Combination of B by A13,A81;
then A82:Carrier L1 c= {v} by RLVECT_2:def 8;
then A83:Carrier L1 = {} or Carrier L1 = {v} by ZFMISC_1:39;

A84:for u being Element of V holds L.u = (r*L1 + (1-r)*L2).u
   proof
     let u be Element of V;
A85:  (r*L1 +(1-r)*L2).u = (r*L1).u +((1-r)*L2).u by RLVECT_2:def 12;
      now per cases;
       suppose
A86:   u in Carrier L;
        now per cases;
         suppose A87:u = v;
         then L1.u = 1 by A83,CONVEX1:21,27;
then A88:      r*L1.u = r;
          u in {v} by A87,TARSKI:def 1;
         then not u in Carrier L2 by A44,XBOOLE_0:def 4;
         then L2.u = 0 by RLVECT_2:28;
         then (1-r)*L2.u = 0;
then A89:      ((1-r)*L2).u = 0 by RLVECT_2:def 13;
          L.u = r + 0 by A3,A15,A87;
         hence thesis by A85,A88,A89,RLVECT_2:def 13;

         suppose u <> v;
then A90:     not u in Carrier L1 by A82,TARSKI:def 1;
         then L1.u = 0 by RLVECT_2:28;
         then r*L1.u = 0;
then A91:     (r*L1).u = 0 by RLVECT_2:def 13;
          u in Carrier L2 by A44,A83,A86,A90,CONVEX1:21,XBOOLE_0:def 4;
         then L2.u = r'*(L.u) by A2,A35,A44;
         then (1-r)*L2.u = ((1-r)*r')*L.u by XCMPLX_1:4
          .= 1/((1-r)/(1-r))*L.u by XCMPLX_1:82
          .= 1*L.u by A31,XCMPLX_1:51
          .= L.u;
         hence thesis by A85,A91,RLVECT_2:def 13;
       end;
       hence thesis;

       suppose A92:not u in Carrier L;
then A93:    L.u = 0 + 0 by RLVECT_2:28;
        not u in Carrier L1 by A2,A12,A82,A92,TARSKI:def 1;
       then L1.u = 0 by RLVECT_2:28;
       then r*L1.u = 0;
then A94:    (r*L1).u = 0 by RLVECT_2:def 13;
        not u in Carrier L2 by A44,A92,XBOOLE_0:def 4;
       then L2.u = 0 by RLVECT_2:28;
       then (1-r)*L2.u = 0;
       hence thesis by A85,A93,A94,RLVECT_2:def 13;
     end;
     hence thesis;
   end;
   take L1,L2,r;
    {v} c= Carrier L by A14,ZFMISC_1:37;
   then card Carrier L2 = card Carrier L - card {v} by A44,CARD_2:63;
   hence thesis by A16,A83,A84,CARD_1:79,CONVEX1:21,RLVECT_2:def 11;
end;

Lm3:
for V being RealLinearSpace, M being non empty Subset of V st
 M is convex holds
  {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M
proof
   let V be RealLinearSpace;
   let M be non empty Subset of V;
   assume
A1:M is convex;
   set S = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
    for v being set st v in S holds v in M
   proof
     let v being set;
     assume v in S;
     then consider L being Convex_Combination of M such that
A2:  v = Sum(L) & L in ConvexComb(V);
     reconsider v as VECTOR of V by A2;
      now per cases;
       suppose card Carrier(L) < 2;
       then card Carrier(L) < 1 + 1;
then A3:    card Carrier(L) <= 1 by NAT_1:38;
        card Carrier(L) <> 0
       proof
         assume card Carrier(L) = 0;
         then Carrier(L) = {} by CARD_2:59;
         hence contradiction by CONVEX1:21;
       end;
       then card Carrier(L) > 0 by NAT_1:19;
       then card Carrier(L) >= 0 + 1 by NAT_1:38;
       then card Carrier(L) = 1 by A3,AXIOMS:21;
       then consider x being set such that
A4:    Carrier(L) = {x} by CARD_2:60;
        x in Carrier(L) by A4,TARSKI:def 1;
       then reconsider x as VECTOR of V;
A5:    v = L.x*x by A2,A4,RLVECT_2:53
        .= 1*x by A4,CONVEX1:27
        .= x by RLVECT_1:def 9;
        {x} c= M by A4,RLVECT_2:def 8;
       hence thesis by A5,ZFMISC_1:37;

       suppose
A6:    card Carrier(L) >= 2;

       defpred P[Nat] means
       for LL being Convex_Combination of M st card Carrier LL = 1 + $1 &
        (ex L1,L2 being Convex_Combination of M, r being Real st
         0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
         card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1)
          holds Sum LL in M;

A7:    P[1]
       proof
         let LL be Convex_Combination of M;
         assume that
A8:      card Carrier LL = 1 + 1 and
A9:      ex L1,L2 being Convex_Combination of M, r being Real st
          0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
          card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1;
         consider L1,L2 be Convex_Combination of M, r be Real such that
A10:      0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
         card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 by A9;
         consider x1 being set such that
A11:      Carrier(L1) = {x1} by A10,CARD_2:60;
          x1 in Carrier(L1) by A11,TARSKI:def 1;
         then reconsider x1 as VECTOR of V;
          Sum L1 = L1.x1 * x1 & L1.x1 = 1 by A11,CONVEX1:27,RLVECT_2:53;
then A12:      Sum L1 = x1 by RLVECT_1:def 9;
A13:      {x1} c= M by A11,RLVECT_2:def 8;
         consider x2 being set such that
A14:      Carrier(L2) = {x2} by A8,A10,CARD_2:60;
          x2 in Carrier(L2) by A14,TARSKI:def 1;
         then reconsider x2 as VECTOR of V;
          Sum L2 = L2.x2 * x2 & L2.x2 = 1 by A14,CONVEX1:27,RLVECT_2:53;
then A15:      Sum L2 = x2 by RLVECT_1:def 9;
          {x2} c= M by A14,RLVECT_2:def 8;
then A16:      Sum L1 in M & Sum L2 in M by A12,A13,A15,ZFMISC_1:37;

          Sum LL = Sum(r*L1) + Sum((1-r)*L2) by A10,RLVECT_3:1
          .= r*Sum L1 + Sum((1-r)*L2) by RLVECT_3:2
          .= r*Sum L1 + (1-r)*Sum L2 by RLVECT_3:2;
         hence Sum LL in M by A1,A10,A16,CONVEX1:def 2;
       end;

A17:    for k being non empty Nat st P[k] holds P[k+1]
       proof
         let k being non empty Nat;
         assume
A18:      P[k];
         let LL be Convex_Combination of M;
         assume that
A19:      card Carrier LL = 1 + (k+1) and
A20:      ex L1,L2 being Convex_Combination of M, r being Real st
          0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
          card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1;
         consider L1,L2 be Convex_Combination of M, r be Real such that
A21:      0 < r & r < 1 & LL = r*L1 + (1-r)*L2 &
         card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 by A20;
         consider x1 being set such that
A22:      Carrier(L1) = {x1} by A21,CARD_2:60;
          x1 in Carrier(L1) by A22,TARSKI:def 1;
         then reconsider x1 as VECTOR of V;
          Sum L1 = L1.x1 * x1 & L1.x1 = 1 by A22,CONVEX1:27,RLVECT_2:53;
then A23:      Sum L1 = x1 by RLVECT_1:def 9;
          {x1} c= M by A22,RLVECT_2:def 8;
then A24:      Sum L1 in M by A23,ZFMISC_1:37;

A25:      card Carrier(L2) = (k+1) + (1-1) by A19,A21,XCMPLX_1:29
          .= k + 1;
          k > 0 by NAT_1:19;
         then k >= 0 + 1 by NAT_1:38;
then k + 1 >= 1 + 1 by AXIOMS:24;
         then consider LL1,LL2 be Convex_Combination of M, rr be Real such that
A26:      0 < rr & rr < 1 & L2 = rr*LL1 + (1-rr)*LL2 & card Carrier(LL1) = 1 &
          card Carrier(LL2) = card Carrier(L2) - 1 by A25,Lm2;

A27:     Sum L2 in M by A18,A25,A26;

          Sum LL = Sum(r*L1) + Sum((1-r)*L2) by A21,RLVECT_3:1
          .= r*Sum L1 + Sum((1-r)*L2) by RLVECT_3:2
          .= r*Sum L1 + (1-r)*Sum L2 by RLVECT_3:2;
         hence Sum LL in M by A1,A21,A24,A27,CONVEX1:def 2;
       end;
A28:    for k being non empty Nat holds P[k] from Ind_from_1(A7,A17);
        card Carrier(L) <> 0 by A6;
       then ex k being Nat st card Carrier L = k + 1 by NAT_1:22;
       then consider k being Nat such that
A29:   card Carrier L = 1 + k;
        k <> 0 by A6,A29;
       then reconsider k as non empty Nat;
A30:   card Carrier L = 1 + k by A29;
        ex L1,L2 being Convex_Combination of M, r being Real st
       0 < r & r < 1 & L = r*L1 + (1-r)*L2 & card Carrier(L1) = 1 &
       card Carrier(L2) = card Carrier(L) - 1 by A6,Lm2;
       hence thesis by A2,A28,A30;
     end;
     hence thesis;
   end;
   hence thesis by TARSKI:def 3;
end;

theorem
 for V being RealLinearSpace, M being non empty Subset of V holds
 M is convex iff
  {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c= M
   by Lm1,Lm3;

theorem
 for V being RealLinearSpace, M being non empty Subset of V holds
 conv(M) = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}
proof
   let V be RealLinearSpace;
   let M be non empty Subset of V;
    for x being set st
    x in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}
     holds x in conv(M)
   proof
     let x be set;
     assume
      x in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)};
     then consider L being Convex_Combination of M such that
A1:  x = Sum(L) & L in ConvexComb(V);
      M c= conv(M) by CONVEX2:8;
     hence thesis by A1,CONVEX2:6;
   end;
then A2:{Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)} c=
conv(M)
    by TARSKI:def 3;
   consider m being set such that
A3:m in M by XBOOLE_0:def 1;

   reconsider m as VECTOR of V by A3;
   consider LL being Convex_Combination of V such that
A4:Sum LL = m &
   for A being non empty Subset of V st m in A holds
    LL is Convex_Combination of A by Th1;
   reconsider LL as Convex_Combination of M by A3,A4;
    LL in ConvexComb(V) by Def1;
   then m in {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}
    by A4;
   then reconsider
    N = {Sum(L) where L is Convex_Combination of M : L in ConvexComb(V)}
     as non empty set;
    for x being set st x in N holds x in the carrier of V
   proof
     let x be set;
     assume x in N;
     then consider L being Convex_Combination of M such that
A5:  x = Sum L & L in ConvexComb(V);
     thus thesis by A5;
   end;
   then N c= the carrier of V by TARSKI:def 3;
   then reconsider N as Subset of V;
    for u,v being VECTOR of V,
     r be Real st 0 < r & r < 1 & u in N & v in N holds
     r*u + (1-r)*v in N
   proof
     let u,v be VECTOR of V;
     let r be Real;
     assume
A6:  0 < r & r < 1 & u in N & v in N;
     then consider Lu being Convex_Combination of M such that
A7:  u = Sum Lu & Lu in ConvexComb(V);
     consider Lv being Convex_Combination of M such that
A8:  v = Sum Lv & Lv in ConvexComb(V) by A6;
      r*Lu + (1-r)*Lv is Convex_Combination of V by A6,CONVEX2:9;
then A9: r*Lu + (1-r)*Lv in ConvexComb(V) by Def1;

     reconsider LL = r*Lu + (1-r)*Lv as Convex_Combination of M
      by A6,CONVEX2:10;
      Sum LL = Sum(r*Lu) + Sum((1-r)*Lv) by RLVECT_3:1
      .= r*Sum Lu + Sum((1-r)*Lv) by RLVECT_3:2
      .= r*Sum Lu + (1-r)*Sum Lv by RLVECT_3:2;
     hence r*u + (1-r)*v in N by A7,A8,A9;
   end;
then A10:N is convex by CONVEX1:def 2;

    for v being set st v in M holds v in N
   proof
     let v be set;
     assume
A11: v in M;
     then reconsider v as VECTOR of V;
     consider LL being Convex_Combination of V such that
A12:  Sum LL = v &
     for A being non empty Subset of V st v in A holds
      LL is Convex_Combination of A by Th1;
     reconsider LL as Convex_Combination of M by A11,A12;
      LL in ConvexComb(V) by Def1;
     hence thesis by A12;
   end;

   then M c= N by TARSKI:def 3;
   then conv(M) c= N by A10,CONVEX1:30;
   hence thesis by A2,XBOOLE_0:def 10;
end;

begin :: Cone and Convex Cone

definition let V be non empty RLSStruct, M be Subset of V;
attr M is cone means :Def3:
 for r being Real, v being VECTOR of V st r > 0 & v in M holds
  r*v in M;
end;

theorem Th6:
for V being non empty RLSStruct, M being Subset of V st
 M = {} holds M is cone
proof
   let V be non empty RLSStruct;
   let M be Subset of V;
   assume
A1:M = {};
    for r being Real, v being VECTOR of V st r > 0 & v in {} holds
    r*v in {};
   hence thesis by A1,Def3;
end;

definition let V be non empty RLSStruct;
cluster cone Subset of V;
existence
proof
  consider M being empty Subset of V;
   M is cone by Th6;
  hence thesis;
end;
end;

definition let V be non empty RLSStruct;
cluster empty cone Subset of V;
existence
proof
   set M = {};
    M c= the carrier of V by XBOOLE_1:2;
   then reconsider M as Subset of V;
   reconsider M as cone Subset of V by Th6;
   take M;
   thus thesis;
end;
end;

definition let V be RealLinearSpace;
cluster non empty cone Subset of V;
existence
proof
   set M = {0.V};
   reconsider M as Subset of V;
    for r being Real, v being VECTOR of V st r > 0 & v in M holds
    r*v in M
   proof
     let r be Real;
     let v be VECTOR of V;
     assume r > 0 & v in M;
     then v = 0.V by TARSKI:def 1;
     then r*v = 0.V by RLVECT_1:23;
     hence thesis by TARSKI:def 1;
   end;
   then reconsider M as cone Subset of V by Def3;
   take M;
   thus thesis by TARSKI:def 1;
end;
end;

theorem Th7:
for V being non empty RLSStruct, M being cone Subset of V st
 V is RealLinearSpace-like holds
  M is convex iff
   for u,v being VECTOR of V st u in M & v in M holds u + v in M
proof
   let V be non empty RLSStruct;
   let M be cone Subset of V;
   assume
A1:V is RealLinearSpace-like;
A2:M is convex implies
    for u,v being VECTOR of V st u in M & v in M holds u + v in M
   proof
     assume
A3:  M is convex;

      for u,v being VECTOR of V st u in M & v in M holds u + v in M
     proof
       let u,v being VECTOR of V;
       assume
    u in M & v in M;
       then (1/2)*u + (1-(1/2))*v in M by A3,CONVEX1:def 2;
then A4:    2*((1/2)*u + (1/2)*v) in M by Def3;

        2*((1/2)*u + (1/2)*v) = 2*((1/2)*u) + 2*((1/2)*v) by A1,RLVECT_1:def 9
        .= (2*(1/2))*u + 2*((1/2)*v) by A1,RLVECT_1:def 9
        .= 1*u + (2*(1/2))*v by A1,RLVECT_1:def 9
        .= u + 1*v by A1,RLVECT_1:def 9;
       hence thesis by A1,A4,RLVECT_1:def 9;
     end;
     hence thesis;
   end;
    (for u,v being VECTOR of V st u in M & v in M holds u + v in M) implies
    M is convex
   proof
     assume
A5:  for u,v being VECTOR of V st u in M & v in M holds u + v in M;

      for u,v being VECTOR of V,
      r be Real st 0 < r & r < 1 & u in M & v in M holds
       r*u + (1-r)*v in M
     proof
       let u,v be VECTOR of V;
       let r be Real;
       assume that
A6:    0 < r & r < 1 and
A7:    u in M & v in M;
        r + 0 < 1 by A6;
       then 1 - r > 0 by REAL_1:86;
       then r*u in M & (1-r)*v in M by A6,A7,Def3;
       hence thesis by A5;
     end;
     hence thesis by CONVEX1:def 2;
   end;
   hence thesis by A2;
end;

Lm4:
for V being RealLinearSpace, M being Subset of V,
 L being Linear_Combination of M st card Carrier(L) >= 1 holds
  ex L1,L2 being Linear_Combination of M st
   Sum L = Sum L1 + Sum L2 & card Carrier(L1) = 1 &
    card Carrier(L2) = card Carrier(L) - 1 &
     Carrier(L1) c= Carrier(L) & Carrier(L2) c= Carrier(L) &
      (for v being VECTOR of V st v in Carrier L1 holds L1.v = L.v) &
      (for v being VECTOR of V st v in Carrier L2 holds L2.v = L.v)
proof
   let V be RealLinearSpace;
   let M be Subset of V;
   let L be Linear_Combination of M;
   assume
card Carrier(L) >= 1;
   then card Carrier L <> 0;
   then Carrier L <> {} by CARD_4:17;
   then consider u being set such that
A1:u in Carrier L by XBOOLE_0:def 1;
   reconsider u as VECTOR of V by A1;

   consider L1 be Linear_Combination of {u} such that
A2:L1.u = L.u from LinCEx1;
    Carrier L c= M by RLVECT_2:def 8;
then A3:{u} c= M by A1,ZFMISC_1:37;
A4:Carrier L1 c= {u} by RLVECT_2:def 8;
   then Carrier L1 c= M by A3,XBOOLE_1:1;
   then reconsider L1 as Linear_Combination of M by RLVECT_2:def 8;
A5:for v being VECTOR of V st v in Carrier L1 holds L1.v = L.v
   proof
     let v be VECTOR of V;
     assume v in Carrier L1;
     then v = u by A4,TARSKI:def 1;
     hence thesis by A2;
   end;

   defpred P[set,set] means
    ($1 in (Carrier L \ {u}) implies $2 = L.$1) &
    (not ($1 in (Carrier L \ {u})) implies $2 = 0);
A6:for x,y1,y2 being set st
    x in the carrier of V & P[x,y1] & P[x,y2]
    holds y1 = y2;

A7:for x being set st x in the carrier of V
    ex y being set st P[x,y]
   proof
     let x be set;
     assume x in the carrier of V;
      x in (Carrier L \ {u}) or not (x in (Carrier L \ {u}));
     hence thesis;
   end;

   consider L2 being Function such that
A8:dom L2 = the carrier of V &
   for x being set st x in the carrier of V holds P[x,L2.x]
     from FuncEx(A6,A7);

    for y being set st y in rng L2 holds y in REAL
   proof
     let y be set;
     assume y in rng L2;
     then consider x being set such that
A9: x in dom L2 & y = L2.x by FUNCT_1:def 5;
      now per cases;
       suppose
A10:   x in (Carrier L \ {u});
       then reconsider x as VECTOR of V;
        y = L.x by A8,A9,A10;
       hence thesis;

       suppose not (x in (Carrier L \ {u}));
       then y = 0 by A8,A9;
       hence thesis;
     end;
     hence thesis;
   end;
   then rng L2 c= REAL by TARSKI:def 3;

then A11:L2 is Element of Funcs(the carrier of V, REAL) by A8,FUNCT_2:def 2;

    ex T being finite Subset of V st
    for v being Element of V st not v in T holds L2.v = 0
   proof
     set T = Carrier(L) \ {u};
     reconsider T as finite Subset of V;
     take T;
     thus thesis by A8;
   end;
   then reconsider L2 as Linear_Combination of V by A11,RLVECT_2:def 5;

    for x being set st x in Carrier L2 holds x in M
   proof
     let x be set;
     assume
A12: x in Carrier L2;
     then reconsider x as VECTOR of V;
      L2.x <> 0 by A12,RLVECT_2:28;
     then x in Carrier L \ {u} by A8;
then A13: x in Carrier L by XBOOLE_0:def 4;
      Carrier L c= M by RLVECT_2:def 8;
     hence thesis by A13;
   end;
   then Carrier L2 c= M by TARSKI:def 3;
   then reconsider L2 as Linear_Combination of M by RLVECT_2:def 8;

    Carrier L1 <> {}
   proof
     assume
      Carrier L1 = {};
     then L.u = 0 by A2,RLVECT_2:28;
     hence contradiction by A1,RLVECT_2:28;
   end;
   then A14:Carrier L1 = {u} by A4,ZFMISC_1:39;

    for x being set st x in Carrier L2 holds x in Carrier L \ {u}
   proof
     let x be set;
     assume
A15: x in Carrier L2;
     then reconsider x as VECTOR of V;
      L2.x <> 0 by A15,RLVECT_2:28;
     hence thesis by A8;
   end;
then A16:Carrier L2 c= Carrier L \ {u} by TARSKI:def 3;
    for x being set st x in Carrier L \ {u} holds x in Carrier L2
   proof
     let x be set;
     assume
A17: x in Carrier L \ {u};
     then reconsider x as VECTOR of V;
A18: L2.x = L.x by A8,A17;
      x in Carrier L by A17,XBOOLE_0:def 4;
     then L.x <> 0 by RLVECT_2:28;
     hence thesis by A18,RLVECT_2:28;
   end;
   then Carrier L \ {u} c= Carrier L2 by TARSKI:def 3;
then A19:Carrier L2 = Carrier L \ {u} by A16,XBOOLE_0:def 10;

    for v being VECTOR of V holds L.v = (L1 + L2).v
   proof
     let v be VECTOR of V;
      now per cases;
       suppose
A20:   v in Carrier L;
        now per cases;
         suppose
A21:     v = u;
then A22:     not v in Carrier L2 by A16,ZFMISC_1:64;
          (L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12
          .= L.v + 0 by A2,A21,A22,RLVECT_2:28;
         hence thesis;

         suppose
A23:     v <> u;
         then not v in Carrier L1 by A4,TARSKI:def 1;
then A24:     L1.v = 0 by RLVECT_2:28;
A25:     v in Carrier L \ {u} by A20,A23,ZFMISC_1:64;
          (L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12
          .= 0 + L.v by A8,A24,A25;
         hence thesis;
       end;
       hence thesis;

       suppose
A26:   not v in Carrier L;
then A27:   not v in Carrier L1 by A1,A4,TARSKI:def 1;
        not v in Carrier L2 by A16,A26,ZFMISC_1:64;
then A28:   L2.v = 0 by RLVECT_2:28;
        (L1 + L2).v = L1.v + L2.v by RLVECT_2:def 12
        .= 0 by A27,A28,RLVECT_2:28;
       hence thesis by A26,RLVECT_2:28;
     end;
     hence thesis;
   end;
then A29:L = L1 + L2 by RLVECT_2:def 11;

     Carrier L1 c= Carrier L by A1,A14,ZFMISC_1:37;
then A30:card Carrier L2 = card Carrier L - card Carrier L1
     by A14,A19,CARD_2:63
     .= card Carrier L - 1 by A14,CARD_1:79;
   take L1,L2;
    Carrier L \ {u} c= Carrier L by XBOOLE_1:36;
   hence thesis by A1,A5,A8,A14,A16,A29,A30,CARD_1:79,RLVECT_3:1,XBOOLE_1:1,
ZFMISC_1:37;
end;

theorem
 for V being RealLinearSpace, M being Subset of V holds
 M is convex & M is cone iff
 (for L being Linear_Combination of M st Carrier L <> {} &
  for v being VECTOR of V st v in Carrier L holds L.v > 0
   holds Sum(L) in M)
proof
   let V be RealLinearSpace;
   let M be Subset of V;
A1:M is convex & M is cone implies
    (for L being Linear_Combination of M st Carrier L <> {} &
     (for v being VECTOR of V st v in Carrier L holds L.v > 0)
      holds Sum(L) in M)
   proof
     assume
A2:  M is convex & M is cone;

     let L be Linear_Combination of M;
     assume
A3:  Carrier L <> {} &
     for v being VECTOR of V st v in Carrier L holds L.v > 0;

     defpred P[Nat] means
     for LL being Linear_Combination of M st card Carrier LL = $1 &
      (for u being VECTOR of V st u in Carrier LL holds LL.u > 0) &
      (ex L1,L2 being Linear_Combination of M st
       Sum LL = Sum L1 + Sum L2 &
        card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 &
         Carrier(L1) c= Carrier LL & Carrier(L2) c= Carrier LL &
         (for v being VECTOR of V st v in Carrier L1 holds L1.v = LL.v) &
         (for v being VECTOR of V st v in Carrier L2 holds L2.v = LL.v))
          holds Sum LL in M;

A4: P[1]
     proof
       let LL be Linear_Combination of M;
       assume that
A5:    card Carrier LL = 1 and
A6:    for u being VECTOR of V st u in Carrier LL holds LL.u > 0 and
        ex L1,L2 being Linear_Combination of M st
        Sum LL = Sum L1 + Sum L2 &
        card Carrier L1 = 1 & card Carrier L2 = card Carrier LL - 1 &
        Carrier(L1) c= Carrier LL & Carrier(L2) c= Carrier LL &
        (for v being VECTOR of V st v in Carrier L1 holds L1.v = LL.v) &
        (for v being VECTOR of V st v in Carrier L2 holds L2.v = LL.v);

       consider x being set such that
A7:    Carrier LL = {x} by A5,CARD_2:60;
        {x} c= M by A7,RLVECT_2:def 8;
then A8:    x in M by ZFMISC_1:37;
       then reconsider x as VECTOR of V;
A9:    Sum LL = LL.x * x by A7,RLVECT_2:53;
        x in Carrier LL by A7,TARSKI:def 1;
       then LL.x > 0 by A6;
       hence thesis by A2,A8,A9,Def3;
     end;

A10: for k being non empty Nat st P[k] holds P[k+1]
     proof
       let k be non empty Nat;
       assume
A11:   P[k];

       let LL be Linear_Combination of M;
       assume that
A12:   card Carrier LL = k + 1 and
A13:   for u being VECTOR of V st u in Carrier LL holds LL.u > 0 and
A14:   ex L1,L2 being Linear_Combination of M st
        Sum LL = Sum L1 + Sum L2 &
        card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 &
        Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL &
        (for v being VECTOR of V st v in Carrier L1 holds L1.v = LL.v) &
        (for v being VECTOR of V st v in Carrier L2 holds L2.v = LL.v);

       consider L1,L2 be Linear_Combination of M such that
A15:   Sum LL = Sum L1 + Sum L2 &
       card Carrier(L1) = 1 & card Carrier(L2) = card Carrier(LL) - 1 &
       Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL &
       (for v being VECTOR of V st v in Carrier L1 holds L1.v = LL.v) &
       (for v being VECTOR of V st v in Carrier L2 holds L2.v = LL.v) by A14;
A16:   card Carrier L2 = k by A12,A15,XCMPLX_1:26;
       then card Carrier L2 > 0 by NAT_1:19;
       then card Carrier L2 >= 0 + 1 by NAT_1:38;

then A17:   ex LL1,LL2 being Linear_Combination of M st
        Sum L2 = Sum LL1 + Sum LL2 & card Carrier LL1 = 1 &
        card Carrier LL2 = card Carrier L2 - 1 &
        Carrier LL1 c= Carrier L2 & Carrier LL2 c= Carrier L2 &
        (for v being VECTOR of V st v in Carrier LL1 holds LL1.v = L2.v) &
        (for v being VECTOR of V st v in Carrier LL2 holds LL2.v = L2.v)
        by Lm4;

        for u being VECTOR of V st u in Carrier L2 holds L2.u > 0
       proof
         let u be VECTOR of V;
         assume u in Carrier L2;
         then u in Carrier LL & L2.u = LL.u by A15;
         hence thesis by A13;
       end;
then A18:   Sum L2 in M by A11,A16,A17;

A19:   ex LL1,LL2 being Linear_Combination of M st
        Sum L1 = Sum LL1 + Sum LL2 & card Carrier LL1 = 1 &
        card Carrier LL2 = card Carrier L1 - 1 &
        Carrier LL1 c= Carrier L1 & Carrier LL2 c= Carrier L1 &
        (for v being VECTOR of V st v in Carrier LL1 holds LL1.v = L1.v) &
        (for v being VECTOR of V st v in Carrier LL2 holds LL2.v = L1.v)
        by A15,Lm4;
        for u being VECTOR of V st u in Carrier L1 holds L1.u > 0
       proof
         let u be VECTOR of V;
         assume u in Carrier L1;
         then u in Carrier LL & L1.u = LL.u by A15;
         hence thesis by A13;
       end;
       then Sum L1 in M by A4,A15,A19;
       hence thesis by A2,A15,A18,Th7;
     end;

A20:  for k being non empty Nat holds P[k] from Ind_from_1(A4,A10);

A21:  card Carrier L <> 0 by A3,CARD_2:59;
     then card Carrier L > 0 by NAT_1:19;
     then card Carrier L >= 0 + 1 by NAT_1:38;
then A22:  ex L1,L2 being Linear_Combination of M st
     Sum L = Sum L1 + Sum L2 & card Carrier L1 = 1 &
     card Carrier L2 = card Carrier L - 1 &
     Carrier L1 c= Carrier L & Carrier L2 c= Carrier L &
     (for v being VECTOR of V st v in Carrier L1 holds L1.v = L.v) &
     (for v being VECTOR of V st v in Carrier L2 holds L2.v = L.v)
     by Lm4;

     consider k being non empty Nat such that
A23:  card Carrier L = k by A21;
     thus thesis by A3,A20,A22,A23;
   end;

    (for L being Linear_Combination of M st
    Carrier L <> {} &
    for v being VECTOR of V st v in Carrier L holds L.v > 0
     holds Sum(L) in M)
   implies M is convex & M is cone
   proof
     assume
A24:  (for L being Linear_Combination of M st
      Carrier L <> {} &
      for v being VECTOR of V st v in Carrier L holds L.v > 0
      holds Sum(L) in M);

A25:  for r being Real, v being VECTOR of V st r > 0 & v in M holds r*v in M
     proof
       let r be Real;
       let v be VECTOR of V;
       assume
A26:    r > 0 & v in M;

       consider L being Linear_Combination of {v} such that
A27:    L.v = r from LinCEx1;

A28:    v in Carrier L by A26,A27,RLVECT_2:28;
A29:    for u being VECTOR of V st u in Carrier L holds L.u > 0
       proof
         let u be VECTOR of V;
         assume
A30:      u in Carrier L;
          Carrier L c= {v} by RLVECT_2:def 8;
         hence thesis by A26,A27,A30,TARSKI:def 1;
       end;
        {v} c= M by A26,ZFMISC_1:37;
       then reconsider L as Linear_Combination of M by RLVECT_2:33;
        Sum L in M by A24,A28,A29;
       hence thesis by A27,RLVECT_2:50;
     end;
then A31:  M is cone by Def3;

      for u,v being VECTOR of V st u in M & v in M holds u + v in M
     proof
       let u,v be VECTOR of V;
       assume
A32:    u in M & v in M;

        now per cases;
         suppose
A33:      u <> v;
         consider L being Linear_Combination of {u,v} such that
A34:     L.u = 1 & L.v = 1 from LinCEx2(A33);

A35:     Carrier L <> {} by A34,RLVECT_2:28;

A36:     for v1 being VECTOR of V st v1 in Carrier L holds L.v1 > 0
         proof
           let v1 be VECTOR of V;
           assume
A37:       v1 in Carrier L;
A38:       Carrier L c= {u,v} by RLVECT_2:def 8;
            now per cases by A37,A38,TARSKI:def 2;
             suppose v1 = u;
             hence thesis by A34;
             suppose v1 = v;
             hence thesis by A34;
           end;
           hence thesis;
         end;

A39:     Sum L = 1 * u + 1 * v by A33,A34,RLVECT_2:51
          .= u + 1 * v by RLVECT_1:def 9
          .= u + v by RLVECT_1:def 9;
          {u,v} c= M by A32,ZFMISC_1:38;
         then reconsider L as Linear_Combination of M by RLVECT_2:33;
          Sum L in M by A24,A35,A36;
         hence thesis by A39;

         suppose
A40:     u = v;
          (1+1)*u in M by A25,A32;
         then 1*u + 1*u in M by RLVECT_1:def 9;
         then u + 1*u in M by RLVECT_1:def 9;
         hence thesis by A40,RLVECT_1:def 9;
       end;
       hence thesis;
     end;
     hence thesis by A31,Th7;
   end;
   hence thesis by A1;
end;

theorem
 for V being non empty RLSStruct, M,N being Subset of V st
 M is cone & N is cone holds M /\ N is cone
proof
   let V be non empty RLSStruct;
   let M,N be Subset of V;
   assume that
A1:M is cone and
A2:N is cone;
   let r be Real;
   let v be VECTOR of V;
   assume
A3:r > 0 & v in M /\ N;
then A4:v in M & v in N by XBOOLE_0:def 3;
then A5:r*v in M by A1,A3,Def3;
    r*v in N by A2,A3,A4,Def3;
   hence thesis by A5,XBOOLE_0:def 3;
end;

Back to top