simplex1.miz



    begin

    reserve x,y,X for set,

r for Real,

n,k for Nat;

    theorem :: SIMPLEX1:1

    

     Th1: for R be Relation, C be Cardinal st for x be object st x in X holds ( card ( Im (R,x))) = C holds ( card R) = (( card (R | (( dom R) \ X))) +` (C *` ( card X)))

    proof

      let R be Relation, C be Cardinal such that

       A1: for x be object st x in X holds ( card ( Im (R,x))) = C;

      set DA = (( dom R) \ X);

      per cases ;

        suppose

         A2: X c= ( dom R);

        deffunc F( object) = ( Im (R,$1));

        consider f be Function such that

         A3: ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

        defpred P[ object, object] means ex g be Function st g = $2 & ( dom g) = (f . $1) & ( rng g) = C & g is one-to-one;

        

         A4: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in X;

          then (f . x) = ( Im (R,x)) & ( card ( Im (R,x))) = C by A1, A3;

          then ((f . x),C) are_equipotent by CARD_1:def 2;

          then

          consider g be Function such that

           A5: g is one-to-one & ( dom g) = (f . x) & ( rng g) = C by WELLORD2:def 4;

          take g;

          thus thesis by A5;

        end;

        consider ff be Function such that

         A6: ( dom ff) = X & for x be object st x in X holds P[x, (ff . x)] from CLASSES1:sch 1( A4);

        now

          let x be object;

          assume x in ( dom ff);

          then ex g be Function st g = (ff . x) & ( dom g) = (f . x) & ( rng g) = C & g is one-to-one by A6;

          hence (ff . x) is Function;

        end;

        then

        reconsider ff as Function-yielding Function by FUNCOP_1:def 6;

        deffunc G( object) = [($1 `1 ), ((ff . ($1 `1 )) . ($1 `2 ))];

        consider p be Function such that

         A7: ( dom p) = (R | X) & for x be object st x in (R | X) holds (p . x) = G(x) from FUNCT_1:sch 3;

        

         A8: ( rng p) = [:X, C:]

        proof

          hereby

            let y be object;

            assume y in ( rng p);

            then

            consider x be object such that

             A9: x in ( dom p) and

             A10: (p . x) = y by FUNCT_1:def 3;

            

             A11: (p . x) = [(x `1 ), ((ff . (x `1 )) . (x `2 ))] by A7, A9;

            

             A12: x = [(x `1 ), (x `2 )] by A7, A9, MCART_1: 21;

            then (x `1 ) in {(x `1 )} & x in R by A7, A9, RELAT_1:def 11, TARSKI:def 1;

            then

             A13: (x `2 ) in (R .: {(x `1 )}) by A12, RELAT_1:def 13;

            

             A14: (x `1 ) in X by A7, A9, A12, RELAT_1:def 11;

            then

            consider g be Function such that

             A15: g = (ff . (x `1 )) and

             A16: ( dom g) = (f . (x `1 )) and

             A17: ( rng g) = C and g is one-to-one by A6;

            (f . (x `1 )) = ( Im (R,(x `1 ))) by A3, A14;

            then (x `2 ) in ( dom g) by A13, A16, RELAT_1:def 16;

            then (g . (x `2 )) in C by A17, FUNCT_1:def 3;

            hence y in [:X, C:] by A10, A11, A14, A15, ZFMISC_1: 87;

          end;

          let y be object;

          assume y in [:X, C:];

          then

          consider y1,y2 be object such that

           A18: y1 in X and

           A19: y2 in C and

           A20: y = [y1, y2] by ZFMISC_1:def 2;

          consider g be Function such that

           A21: g = (ff . y1) and

           A22: ( dom g) = (f . y1) and

           A23: ( rng g) = C and g is one-to-one by A6, A18;

          consider x2 be object such that

           A24: x2 in ( dom g) and

           A25: (g . x2) = y2 by A19, A23, FUNCT_1:def 3;

          

           A26: G([) = y by A20, A21, A25;

          (f . y1) = ( Im (R,y1)) by A3, A18;

          then [y1, x2] in R by A22, A24, RELSET_2: 9;

          then

           A27: [y1, x2] in (R | X) by A18, RELAT_1:def 11;

          then (p . [y1, x2]) = G([) by A7;

          hence thesis by A7, A26, A27, FUNCT_1:def 3;

        end;

        now

          let x1,x2 be object such that

           A28: x1 in ( dom p) and

           A29: x2 in ( dom p) and

           A30: (p . x1) = (p . x2);

          

           A31: (p . x1) = G(x1) & (p . x2) = G(x2) by A7, A28, A29;

          then

           A32: (x1 `1 ) = (x2 `1 ) by A30, XTUPLE_0: 1;

          

           A33: x1 = [(x1 `1 ), (x1 `2 )] by A7, A28, MCART_1: 21;

          then x1 in R by A7, A28, RELAT_1:def 11;

          then

           A34: (x1 `2 ) in ( Im (R,(x1 `1 ))) by A33, RELSET_2: 9;

          

           A35: x2 = [(x2 `1 ), (x2 `2 )] by A7, A29, MCART_1: 21;

          then x2 in R by A7, A29, RELAT_1:def 11;

          then

           A36: (x2 `2 ) in ( Im (R,(x2 `1 ))) by A35, RELSET_2: 9;

          (x2 `1 ) in X by A7, A29, A35, RELAT_1:def 11;

          then

          consider g2 be Function such that

           A37: g2 = (ff . (x2 `1 )) and ( dom g2) = (f . (x2 `1 )) and ( rng g2) = C and g2 is one-to-one by A6;

          

           A38: (x1 `1 ) in X by A7, A28, A33, RELAT_1:def 11;

          then

          consider g1 be Function such that

           A39: g1 = (ff . (x1 `1 )) and

           A40: ( dom g1) = (f . (x1 `1 )) and ( rng g1) = C and

           A41: g1 is one-to-one by A6;

          

           A42: (f . (x1 `1 )) = ( Im (R,(x1 `1 ))) by A3, A38;

          (g1 . (x1 `2 )) = (g2 . (x2 `2 )) by A30, A31, A37, A39, XTUPLE_0: 1;

          hence x1 = x2 by A32, A35, A36, A33, A34, A37, A39, A40, A41, A42, FUNCT_1:def 4;

        end;

        then p is one-to-one by FUNCT_1:def 4;

        then ((R | X), [:X, C:]) are_equipotent by A7, A8, WELLORD2:def 4;

        

        then

         A43: ( card (R | X)) = ( card [:X, C:]) by CARD_1: 5

        .= ( card [:( card X), C:]) by CARD_2: 7

        .= (C *` ( card X)) by CARD_2:def 2;

        

         A44: (R | X) misses (R | DA)

        proof

          assume (R | X) meets (R | DA);

          then

          consider x be object such that

           A45: x in (R | X) and

           A46: x in (R | DA) by XBOOLE_0: 3;

          consider x1,x2 be object such that

           A47: x = [x1, x2] by A45, RELAT_1:def 1;

          x1 in X & x1 in DA by A45, A46, A47, RELAT_1:def 11;

          hence contradiction by XBOOLE_0:def 5;

        end;

        (DA \/ X) = (( dom R) \/ X) by XBOOLE_1: 39

        .= ( dom R) by A2, XBOOLE_1: 12;

        

        then ((R | X) \/ (R | DA)) = (R | ( dom R)) by RELAT_1: 78

        .= R;

        hence ( card R) = (( card (R | DA)) +` (C *` ( card X))) by A43, A44, CARD_2: 35;

      end;

        suppose not X c= ( dom R);

        then

        consider x be object such that

         A48: x in X and

         A49: not x in ( dom R);

        ( Im (R,x)) = {}

        proof

          assume ( Im (R,x)) <> {} ;

          then

          consider y be object such that

           A50: y in ( Im (R,x)) by XBOOLE_0:def 1;

           [x, y] in R by A50, RELSET_2: 9;

          hence contradiction by A49, XTUPLE_0:def 12;

        end;

        then

         A51: C = ( card {} ) by A1, A48;

        ( dom R) misses X

        proof

          assume ( dom R) meets X;

          then

          consider x be object such that

           A52: x in ( dom R) and

           A53: x in X by XBOOLE_0: 3;

          ( card ( Im (R,x))) = C by A1, A53;

          then

           A54: ( Im (R,x)) is empty by A51;

          ex y be object st [x, y] in R by A52, XTUPLE_0:def 12;

          hence contradiction by A54, RELSET_2: 9;

        end;

        then

         A55: DA = ( dom R) by XBOOLE_1: 83;

        (C *` ( card X)) = 0 by A51, CARD_2: 20;

        then (( card (R | DA)) +` (C *` ( card X))) = ( card (R | DA)) by CARD_2: 18;

        hence thesis by A55;

      end;

    end;

    theorem :: SIMPLEX1:2

    

     Th2: for Y be non empty finite set st ( card X) = (( card Y) + 1) holds for f be Function of X, Y st f is onto holds ex y st y in Y & ( card (f " {y})) = 2 & for x st x in Y & x <> y holds ( card (f " {x})) = 1

    proof

      let Y be non empty finite set such that

       A1: ( card X) = (( card Y) + 1);

      reconsider XX = X as non empty finite set by A1;

      ( card Y) > 0 ;

      then

      reconsider c1 = (( card Y) - 1) as Element of NAT by NAT_1: 20;

      let f be Function of X, Y such that

       A2: f is onto;

      

       A3: ( rng f) = Y by A2, FUNCT_2:def 3;

      reconsider F = f as Function of XX, Y;

      

       A4: ( dom f) = X by FUNCT_2:def 1;

      ex y st y in Y & ( card (F " {y})) > 1

      proof

        assume

         A5: for y st y in Y holds ( card (F " {y})) <= 1;

        now

          let y be object;

          set fy = (F " {y});

          assume

           A6: y in Y;

          then fy <> {} by A3, FUNCT_1: 72;

          then ( card fy) = 1 by A5, A6, NAT_1: 25;

          hence ex x be object st fy = {x} by CARD_2: 42;

        end;

        then f is one-to-one by A3, FUNCT_1: 74;

        then (X,Y) are_equipotent by A3, A4, WELLORD2:def 4;

        then ( card X) = ( card Y) by CARD_1: 5;

        hence contradiction by A1;

      end;

      then

      consider y such that

       A7: y in Y and

       A8: ( card (F " {y})) > 1;

      set fy = (F " {y});

      set fD = (F | (( dom f) \ fy));

      take y;

      

       A9: (1 + 1) <= ( card fy) by A8, NAT_1: 13;

      ( dom fD) = (( dom f) \ fy) by RELAT_1: 62, XBOOLE_1: 36;

      then

       A10: ( card ( dom fD)) = (( card XX) - ( card fy)) by A4, CARD_2: 44;

      set Yy = (Y \ {y});

      

       A11: ( rng fD) = Yy by A3, STIRL2_1: 54;

      then

      reconsider FD = fD as Function of ( dom fD), Yy by FUNCT_2: 1;

      ( card Y) = (c1 + 1);

      then

       A12: ( card Yy) = c1 by A7, STIRL2_1: 55;

      then ( Segm c1) c= ( Segm ( card ( dom fD))) by A11, CARD_1: 12;

      then (( card Y) + ( - 1)) <= (( card Y) + (1 - ( card fy))) by A1, A10, NAT_1: 39;

      then ( - 1) <= (1 - ( card fy)) by XREAL_1: 6;

      then ( card fy) <= (1 - ( - 1)) by XREAL_1: 11;

      hence

       A13: y in Y & ( card (f " {y})) = 2 by A7, A9, XXREAL_0: 1;

      let x such that

       A14: x in Y and

       A15: x <> y;

      

       A16: x in ( rng FD) by A11, A14, A15, ZFMISC_1: 56;

      FD is onto by A11, FUNCT_2:def 3;

      then FD is one-to-one by A1, A10, A12, A13, FINSEQ_4: 63;

      then

       A17: ex z be object st (FD " {x}) = {z} by A16, FUNCT_1: 74;

      (FD " {x}) = (f " {x}) by A15, STIRL2_1: 54;

      hence thesis by A17, CARD_1: 30;

    end;

    definition

      let X be 1-sorted;

      mode SimplicialComplexStr of X is SimplicialComplexStr of the carrier of X;

      mode SimplicialComplex of X is SimplicialComplex of the carrier of X;

    end

    definition

      let X be 1-sorted;

      let K be SimplicialComplexStr of X;

      let A be Subset of K;

      :: SIMPLEX1:def1

      func @ A -> Subset of X equals A;

      coherence

      proof

        ( [#] K) c= the carrier of X by SIMPLEX0:def 9;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    definition

      let X be 1-sorted;

      let K be SimplicialComplexStr of X;

      let A be Subset-Family of K;

      :: SIMPLEX1:def2

      func @ A -> Subset-Family of X equals A;

      coherence

      proof

        ( [#] K) c= the carrier of X by SIMPLEX0:def 9;

        then ( bool ( [#] K)) c= ( bool the carrier of X) by ZFMISC_1: 67;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    theorem :: SIMPLEX1:3

    

     Th3: for X be 1-sorted holds for K be subset-closed SimplicialComplexStr of X st K is total holds for S be finite Subset of K st S is simplex-like holds ( Complex_of {( @ S)}) is SubSimplicialComplex of K

    proof

      let X be 1-sorted;

      let K be subset-closed SimplicialComplexStr of X such that

       A1: K is total;

      let S be finite Subset of K such that

       A2: S is simplex-like;

      S in the topology of K by A2;

      then

       A3: {S} c= the topology of K by ZFMISC_1: 31;

      set C = ( Complex_of {( @ S)});

      

       A4: ( [#] C) c= ( [#] K) by A1;

      ( the_family_of K) is subset-closed;

      then the topology of C c= the topology of K by A3, SIMPLEX0:def 1;

      hence thesis by A4, SIMPLEX0:def 13;

    end;

    begin

    reserve RLS for non empty RLSStruct,

Kr,K1r,K2r for SimplicialComplexStr of RLS,

V for RealLinearSpace,

Kv for non void SimplicialComplex of V;

    definition

      let RLS, Kr;

      :: SIMPLEX1:def3

      func |.Kr.| -> Subset of RLS means

      : Def3: x in it iff ex A be Subset of Kr st A is simplex-like & x in ( conv ( @ A));

      existence

      proof

        set KC = { ( conv ( @ A)) where A be Subset of Kr : A is simplex-like };

        KC c= ( bool the carrier of RLS)

        proof

          let x be object;

          assume x in KC;

          then ex A be Subset of Kr st x = ( conv ( @ A)) & A is simplex-like;

          hence thesis;

        end;

        then

        reconsider KC as Subset-Family of RLS;

        take IT = ( union KC);

        let x;

        hereby

          assume x in IT;

          then

          consider y such that

           A1: x in y and

           A2: y in KC by TARSKI:def 4;

          consider A be Subset of Kr such that

           A3: y = ( conv ( @ A)) & A is simplex-like by A2;

          take A;

          thus A is simplex-like & x in ( conv ( @ A)) by A1, A3;

        end;

        given A be Subset of Kr such that

         A4: A is simplex-like and

         A5: x in ( conv ( @ A));

        ( conv ( @ A)) in KC by A4;

        hence thesis by A5, TARSKI:def 4;

      end;

      uniqueness

      proof

        let S1,S2 be Subset of RLS such that

         A6: x in S1 iff ex A be Subset of Kr st A is simplex-like & x in ( conv ( @ A)) and

         A7: x in S2 iff ex A be Subset of Kr st A is simplex-like & x in ( conv ( @ A));

        now

          let x be object;

          x in S1 iff ex A be Subset of Kr st A is simplex-like & x in ( conv ( @ A)) by A6;

          hence x in S1 iff x in S2 by A7;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: SIMPLEX1:4

    

     Th4: the topology of K1r c= the topology of K2r implies |.K1r.| c= |.K2r.|

    proof

      assume

       A1: the topology of K1r c= the topology of K2r;

      let x be object;

      assume x in |.K1r.|;

      then

      consider A be Subset of K1r such that

       A2: A is simplex-like and

       A3: x in ( conv ( @ A)) by Def3;

      

       A4: A in the topology of K1r by A2;

      then A in the topology of K2r by A1;

      then

      reconsider A1 = A as Subset of K2r;

      ( @ A) = ( @ A1) & A1 is simplex-like by A1, A4;

      hence thesis by A3, Def3;

    end;

    theorem :: SIMPLEX1:5

    

     Th5: for A be Subset of Kr st A is simplex-like holds ( conv ( @ A)) c= |.Kr.| by Def3;

    theorem :: SIMPLEX1:6

    for K be subset-closed SimplicialComplexStr of V holds x in |.K.| iff ex A be Subset of K st A is simplex-like & x in ( Int ( @ A))

    proof

      let K be subset-closed SimplicialComplexStr of V;

      hereby

        assume x in |.K.|;

        then

        consider A be Subset of K such that

         A1: A is simplex-like and

         A2: x in ( conv ( @ A)) by Def3;

        ( conv ( @ A)) = ( union { ( Int B) where B be Subset of V : B c= ( @ A) }) by RLAFFIN2: 8;

        then

        consider IB be set such that

         A3: x in IB and

         A4: IB in { ( Int B) where B be Subset of V : B c= ( @ A) } by A2, TARSKI:def 4;

        consider B be Subset of V such that

         A5: IB = ( Int B) and

         A6: B c= ( @ A) by A4;

        reconsider B1 = B as Subset of K by A6, XBOOLE_1: 1;

        take B1;

        A in the topology of K by A1;

        then K is non void by PENCIL_1:def 4;

        hence B1 is simplex-like & x in ( Int ( @ B1)) by A1, A3, A5, A6, MATROID0: 1;

      end;

      given A be Subset of K such that

       A7: A is simplex-like and

       A8: x in ( Int ( @ A));

      x in ( conv ( @ A)) by A8, RLAFFIN2:def 1;

      hence thesis by A7, Def3;

    end;

    theorem :: SIMPLEX1:7

    

     Th7: |.Kr.| is empty iff Kr is empty-membered

    proof

      hereby

        assume

         A1: |.Kr.| is empty;

        assume Kr is with_non-empty_element;

        then the topology of Kr is with_non-empty_element;

        then

        consider x be non empty set such that

         A2: x in the topology of Kr;

        reconsider X = x as Subset of Kr by A2;

        (ex y be object st y in ( conv ( @ X))) & X is simplex-like by A2, XBOOLE_0:def 1;

        hence contradiction by A1, Def3;

      end;

      assume

       A3: Kr is empty-membered;

      assume |.Kr.| is non empty;

      then

      consider x be object such that

       A4: x in |.Kr.|;

      consider A be Subset of Kr such that

       A5: A is simplex-like & x in ( conv ( @ A)) by A4, Def3;

      A is non empty & A in the topology of Kr by A5;

      then the topology of Kr is with_non-empty_element;

      hence contradiction by A3;

    end;

    theorem :: SIMPLEX1:8

    

     Th8: for A be Subset of RLS holds |.( Complex_of {A}).| = ( conv A)

    proof

      let A be Subset of RLS;

      set C = ( Complex_of {A});

      reconsider A1 = A as Subset of C;

      

       A1: the topology of C = ( bool A) by SIMPLEX0: 4;

      hereby

        let x be object;

        assume x in |.C.|;

        then

        consider S be Subset of C such that

         A2: S is simplex-like and

         A3: x in ( conv ( @ S)) by Def3;

        S in the topology of C by A2;

        then ( conv ( @ S)) c= ( conv A) by A1, RLAFFIN1: 3;

        hence x in ( conv A) by A3;

      end;

      A c= A;

      then ( @ A1) = A & A1 is simplex-like by A1;

      hence thesis by Th5;

    end;

    theorem :: SIMPLEX1:9

    for A,B be Subset-Family of RLS holds |.( Complex_of (A \/ B)).| = ( |.( Complex_of A).| \/ |.( Complex_of B).|)

    proof

      let A,B be Subset-Family of RLS;

      set CA = ( Complex_of A), CB = ( Complex_of B), CAB = ( Complex_of (A \/ B));

      

       A1: (the topology of CA \/ the topology of CB) = the topology of CAB by SIMPLEX0: 5;

      thus |.CAB.| c= ( |.CA.| \/ |.CB.|)

      proof

        let x be object;

        assume x in |.CAB.|;

        then

        consider S be Subset of CAB such that

         A2: S is simplex-like and

         A3: x in ( conv ( @ S)) by Def3;

        

         A4: S in the topology of CAB by A2;

        per cases by A1, A4, XBOOLE_0:def 3;

          suppose

           A5: S in the topology of CA;

          reconsider S1 = S as Subset of CA;

          ( @ S) = ( @ S1) & S1 is simplex-like by A5;

          then ( conv ( @ S)) c= |.CA.| by Th5;

          hence thesis by A3, XBOOLE_0:def 3;

        end;

          suppose

           A6: S in the topology of CB;

          reconsider S1 = S as Subset of CB;

          ( @ S) = ( @ S1) & S1 is simplex-like by A6;

          then ( conv ( @ S)) c= |.CB.| by Th5;

          hence thesis by A3, XBOOLE_0:def 3;

        end;

      end;

       |.CA.| c= |.CAB.| & |.CB.| c= |.CAB.| by A1, Th4, XBOOLE_1: 7;

      hence thesis by XBOOLE_1: 8;

    end;

    begin

    definition

      let RLS, Kr;

      :: SIMPLEX1:def4

      mode SubdivisionStr of Kr -> SimplicialComplexStr of RLS means

      : Def4: |.Kr.| c= |.it .| & for A be Subset of it st A is simplex-like holds ex B be Subset of Kr st B is simplex-like & ( conv ( @ A)) c= ( conv ( @ B));

      existence

      proof

        take Kr;

        thus thesis;

      end;

    end

    theorem :: SIMPLEX1:10

    

     Th10: for P be SubdivisionStr of Kr holds |.Kr.| = |.P.|

    proof

      let P be SubdivisionStr of Kr;

      thus |.Kr.| c= |.P.| by Def4;

      let x be object;

      assume x in |.P.|;

      then

      consider A be Subset of P such that

       A1: A is simplex-like and

       A2: x in ( conv ( @ A)) by Def3;

      ex B be Subset of Kr st B is simplex-like & ( conv ( @ A)) c= ( conv ( @ B)) by A1, Def4;

      hence thesis by A2, Def3;

    end;

    registration

      let RLS;

      let Kr be with_non-empty_element SimplicialComplexStr of RLS;

      cluster -> with_non-empty_element for SubdivisionStr of Kr;

      coherence

      proof

        let P be SubdivisionStr of Kr;

         |.Kr.| is non empty & |.Kr.| = |.P.| by Th7, Th10;

        hence thesis by Th7;

      end;

    end

    theorem :: SIMPLEX1:11

    

     Th11: Kr is SubdivisionStr of Kr

    proof

      thus |.Kr.| c= |.Kr.|;

      thus thesis;

    end;

    theorem :: SIMPLEX1:12

    

     Th12: ( Complex_of the topology of Kr) is SubdivisionStr of Kr

    proof

      set TOP = the topology of Kr;

      set C = ( Complex_of TOP);

      ( [#] C) = ( [#] Kr) & ( [#] Kr) c= the carrier of RLS by SIMPLEX0:def 9;

      then

      reconsider C as SimplicialComplexStr of RLS by SIMPLEX0:def 9;

      

       A1: |.Kr.| c= |.C.|

      proof

        let x be object;

        assume x in |.Kr.|;

        then

        consider A be Subset of Kr such that

         A2: A is simplex-like and

         A3: x in ( conv ( @ A)) by Def3;

        reconsider B = A as Subset of C;

        A in TOP by A2;

        then A in the topology of C by SIMPLEX0: 2;

        then

         A4: B is simplex-like;

        ( @ A) = ( @ B);

        hence thesis by A3, A4, Def3;

      end;

      for A be Subset of C st A is simplex-like holds ex B be Subset of Kr st B is simplex-like & ( conv ( @ A)) c= ( conv ( @ B))

      proof

        let A be Subset of C;

        assume A is simplex-like;

        then A in the topology of C;

        then

        consider B be set such that

         A5: A c= B and

         A6: B in TOP by SIMPLEX0: 2;

        reconsider B as Subset of Kr by A6;

        take B;

        thus thesis by A5, A6, RLAFFIN1: 3;

      end;

      hence thesis by A1, Def4;

    end;

    theorem :: SIMPLEX1:13

    

     Th13: for K be subset-closed SimplicialComplexStr of V holds for SF be Subset-Family of K st SF = ( Sub_of_Fin the topology of K) holds ( Complex_of SF) is SubdivisionStr of K

    proof

      let K be subset-closed SimplicialComplexStr of V;

      set TOP = the topology of K;

      let SF be Subset-Family of K such that

       A1: SF = ( Sub_of_Fin TOP);

      set C = ( Complex_of SF);

      ( [#] C) = ( [#] K) & ( [#] K) c= the carrier of V by SIMPLEX0:def 9;

      then

      reconsider C as SimplicialComplexStr of V by SIMPLEX0:def 9;

      

       A2: ( the_family_of K) is subset-closed;

      then

       A3: the topology of C = SF by A1, SIMPLEX0: 7;

      C is SubdivisionStr of K

      proof

        thus |.K.| c= |.C.|

        proof

          let x be object;

          assume x in |.K.|;

          then

          consider S be Subset of K such that

           A4: S is simplex-like and

           A5: x in ( conv ( @ S)) by Def3;

          reconsider S1 = ( @ S) as non empty Subset of V by A5;

          x in { ( Sum L) where L be Convex_Combination of S1 : L in ( ConvexComb V) } by A5, CONVEX3: 5;

          then

          consider L be Convex_Combination of S1 such that

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

          reconsider Carr = ( Carrier L) as non empty Subset of V by CONVEX1: 21;

          

           A7: Carr c= S by RLVECT_2:def 6;

          then

          reconsider Carr1 = Carr as Subset of C by XBOOLE_1: 1;

          S in TOP by A4;

          then Carr1 in TOP by A2, A7, CLASSES1:def 1;

          then Carr1 in the topology of C by A1, A3, COHSP_1:def 3;

          then

           A8: Carr1 is simplex-like;

          reconsider LC = L as Linear_Combination of Carr by RLVECT_2:def 6;

          LC is convex;

          then x in { ( Sum M) where M be Convex_Combination of Carr : M in ( ConvexComb V) } by A6;

          then

           A9: x in ( conv Carr) by CONVEX3: 5;

          Carr = ( @ Carr1);

          hence thesis by A8, A9, Def3;

        end;

        let A be Subset of C;

        reconsider B = A as Subset of K;

        assume A is simplex-like;

        then A in the topology of C;

        then

         A10: B is simplex-like by A1, A3;

        ( @ A) = ( @ B);

        hence thesis by A10;

      end;

      hence thesis;

    end;

    theorem :: SIMPLEX1:14

    

     Th14: for P1 be SubdivisionStr of Kr holds for P2 be SubdivisionStr of P1 holds P2 is SubdivisionStr of Kr

    proof

      let P1 be SubdivisionStr of Kr;

      let P2 be SubdivisionStr of P1;

       |.P2.| = |.P1.| by Th10

      .= |.Kr.| by Th10;

      hence |.Kr.| c= |.P2.|;

      let A2 be Subset of P2;

      assume A2 is simplex-like;

      then

      consider A1 be Subset of P1 such that

       A1: A1 is simplex-like and

       A2: ( conv ( @ A2)) c= ( conv ( @ A1)) by Def4;

      ex A be Subset of Kr st A is simplex-like & ( conv ( @ A1)) c= ( conv ( @ A)) by A1, Def4;

      hence thesis by A2, XBOOLE_1: 1;

    end;

    registration

      let V;

      let K be SimplicialComplexStr of V;

      cluster finite-membered subset-closed for SubdivisionStr of K;

      existence

      proof

        reconsider C = ( Complex_of the topology of K) as SubdivisionStr of K by Th12;

        reconsider SF = ( Sub_of_Fin the topology of C) as Subset-Family of C by XBOOLE_1: 1;

        ( Complex_of SF) is SubdivisionStr of C by Th13;

        then

        reconsider CSF = ( Complex_of SF) as SubdivisionStr of K by Th14;

        take CSF;

        thus thesis;

      end;

    end

    definition

      let V;

      let K be SimplicialComplexStr of V;

      mode Subdivision of K is finite-membered subset-closed SubdivisionStr of K;

    end

    theorem :: SIMPLEX1:15

    

     Th15: for K be with_empty_element SimplicialComplex of V st |.K.| c= ( [#] K) holds for B be Function of ( BOOL the carrier of V), the carrier of V st for S be Simplex of K st S is non empty holds (B . S) in ( conv ( @ S)) holds ( subdivision (B,K)) is SubdivisionStr of K

    proof

      let K be with_empty_element SimplicialComplex of V such that

       A1: |.K.| c= ( [#] K);

      let B be Function of ( BOOL the carrier of V), the carrier of V such that

       A2: for S be Simplex of K st S is non empty holds (B . S) in ( conv ( @ S));

      set P = ( subdivision (B,K));

      defpred P[ Nat] means for x holds for A be Simplex of K st x in ( conv ( @ A)) & ( card A) = $1 holds ex S be c=-linear finite simplex-like Subset-Family of K, BS be Subset of P st BS = (B .: S) & x in ( conv ( @ BS)) & ( union S) c= A;

      

       A3: ( dom B) = ( BOOL the carrier of V) by FUNCT_2:def 1;

      

       A4: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A5: P[n];

        let x be set, A be Simplex of K such that

         A6: x in ( conv ( @ A)) and

         A7: ( card A) = (n + 1);

        reconsider A1 = ( @ A) as non empty Subset of V by A6;

        

         A8: ( union {A}) = A by ZFMISC_1: 25;

        

         A9: for P be Subset of K holds P in {A} implies P is simplex-like by TARSKI:def 1;

        then

         A10: {A} is simplex-like;

        

         A11: (B . A1) in ( conv ( @ A)) by A2;

        then

        reconsider BA = (B . A) as Element of V;

        A1 = A;

        then

         A12: A in ( dom B) by A3, ZFMISC_1: 56;

        

         A13: (B .: {A}) = ( Im (B,A)) by RELAT_1:def 16;

        then

         A14: (B .: {A}) = {BA} by A12, FUNCT_1: 59;

        BA in ( conv A1) & ( conv A1) c= |.K.| by A2, Th5;

        then BA in |.K.|;

        then ( [#] P) = ( [#] K) & {BA} is Subset of K by A1, SIMPLEX0:def 20, ZFMISC_1: 31;

        then

        reconsider BY = (B .: {A}) as Subset of P by A12, A13, FUNCT_1: 59;

        per cases ;

          suppose

           A15: x = (B . A);

          now

            let x1,x2 be set;

            assume that

             A16: x1 in {A} and

             A17: x2 in {A};

            x1 = A by A16, TARSKI:def 1;

            hence (x1,x2) are_c=-comparable by A17, TARSKI:def 1;

          end;

          then

          reconsider Y = {A} as c=-linear finite simplex-like Subset-Family of K by A9, ORDINAL1:def 8, TOPS_2:def 1;

          take Y, BY;

          ( conv {BA}) = {BA} by RLAFFIN1: 1;

          hence thesis by A14, A15, TARSKI:def 1, ZFMISC_1: 25;

        end;

          suppose x <> (B . A);

          then

          consider p,w be Element of V, r such that

           A18: p in A and

           A19: w in ( conv (A1 \ {p})) and

           A20: 0 <= r & r < 1 & ((r * BA) + ((1 - r) * w)) = x by A6, A11, RLAFFIN2: 26;

          ( @ (A \ {p})) = (A1 \ {p}) & ( card (A \ {p})) = n by A7, A18, STIRL2_1: 55;

          then

          consider S be c=-linear finite simplex-like Subset-Family of K, BS be Subset of P such that

           A21: BS = (B .: S) and

           A22: w in ( conv ( @ BS)) and

           A23: ( union S) c= (A \ {p}) by A5, A19;

          set S1 = (S \/ {A});

          

           A24: (A \ {p}) c= A by XBOOLE_1: 36;

          then

           A25: ( union S) c= A by A23;

          for x1,x2 be set st x1 in S1 & x2 in S1 holds (x1,x2) are_c=-comparable

          proof

            let x1,x2 be set such that

             A26: x1 in S1 & x2 in S1;

            per cases by A26, XBOOLE_0:def 3;

              suppose x1 in S & x2 in S;

              hence thesis by ORDINAL1:def 8;

            end;

              suppose x1 in S & x2 in {A};

              then x1 c= ( union S) & x2 = A by TARSKI:def 1, ZFMISC_1: 74;

              then x1 c= x2 by A25;

              hence thesis;

            end;

              suppose x2 in S & x1 in {A};

              then x2 c= ( union S) & x1 = A by TARSKI:def 1, ZFMISC_1: 74;

              then x2 c= x1 by A25;

              hence thesis;

            end;

              suppose

               A27: x1 in {A} & x2 in {A};

              then x1 = A by TARSKI:def 1;

              hence thesis by A27, TARSKI:def 1;

            end;

          end;

          then

          reconsider S1 as c=-linear finite simplex-like Subset-Family of K by A10, ORDINAL1:def 8, TOPS_2: 13;

          

           A28: (B .: S1) = (BS \/ BY) by A21, RELAT_1: 120;

          then

          reconsider BS1 = (B .: S1) as Subset of P;

          

           A29: ( conv ( @ BS)) c= ( conv ( @ BS1)) by A28, RLTOPSP1: 20, XBOOLE_1: 7;

          BA in BY by A14, TARSKI:def 1;

          then

           A30: BA in ( @ BS1) by A28, XBOOLE_0:def 3;

          take S1, BS1;

          

           A31: ( @ BS1) c= ( conv ( @ BS1)) by CONVEX1: 41;

          ( union S1) = (( union S) \/ A) by A8, ZFMISC_1: 78

          .= A by A23, A24, XBOOLE_1: 1, XBOOLE_1: 12;

          hence thesis by A20, A22, A29, A30, A31, RLTOPSP1:def 1;

        end;

      end;

      

       A32: P[ 0 qua Nat]

      proof

        let x;

        let A be Simplex of K;

        assume that

         A33: x in ( conv ( @ A)) and

         A34: ( card A) = 0 ;

        ( @ A) is non empty by A33;

        hence thesis by A34;

      end;

      

       A35: for n be Nat holds P[n] from NAT_1:sch 2( A32, A4);

      thus |.K.| c= |.P.|

      proof

        let x be object;

        assume x in |.K.|;

        then

        consider A be Subset of K such that

         A36: A is simplex-like and

         A37: x in ( conv ( @ A)) by Def3;

        reconsider A as Simplex of K by A36;

         P[( card A)] by A35;

        then

        consider S be c=-linear finite simplex-like Subset-Family of K, BS be Subset of P such that

         A38: BS = (B .: S) and

         A39: x in ( conv ( @ BS)) and ( union S) c= A by A37;

        BS is simplex-like by A38, SIMPLEX0:def 20;

        then ( conv ( @ BS)) c= |.P.| by Th5;

        hence thesis by A39;

      end;

      for A be Subset of P st A is simplex-like holds ex B be Subset of K st B is simplex-like & ( conv ( @ A)) c= ( conv ( @ B))

      proof

        let A be Subset of P;

        assume A is simplex-like;

        then

        consider S be c=-linear finite simplex-like Subset-Family of K such that

         A40: A = (B .: S) by SIMPLEX0:def 20;

        per cases ;

          suppose

           A41: S is empty;

          take ( {} K);

          thus thesis by A40, A41;

        end;

          suppose

           A42: S is non empty;

          take U = ( union S);

          

           A43: A c= ( conv ( @ U))

          proof

            let x be object;

            assume x in A;

            then

            consider y be object such that

             A44: y in ( dom B) and

             A45: y in S and

             A46: (B . y) = x by A40, FUNCT_1:def 6;

            reconsider y as Simplex of K by A45, TOPS_2:def 1;

            y <> {} by A44, ZFMISC_1: 56;

            then

             A47: (B . y) in ( conv ( @ y)) by A2;

            ( conv ( @ y)) c= ( conv ( @ U)) by A45, RLTOPSP1: 20, ZFMISC_1: 74;

            hence thesis by A46, A47;

          end;

          U in S by A42, SIMPLEX0: 9;

          hence thesis by A43, CONVEX1: 30, TOPS_2:def 1;

        end;

      end;

      hence thesis;

    end;

    registration

      let V, Kv;

      cluster non void for Subdivision of Kv;

      existence

      proof

        reconsider P = Kv as Subdivision of Kv by Th11;

        take P;

        thus thesis;

      end;

    end

    begin

    definition

      let V, Kv;

      :: SIMPLEX1:def5

      func BCS Kv -> non void Subdivision of Kv equals

      : Def5: ( subdivision (( center_of_mass V),Kv));

      coherence

      proof

        set B = ( center_of_mass V);

        for S be Simplex of Kv st S is non empty holds (B . S) in ( conv ( @ S)) by RLAFFIN2: 16;

        hence thesis by A1, Th15;

      end;

    end

    definition

      let n;

      let V, Kv;

      :: SIMPLEX1:def6

      func BCS (n,Kv) -> non void Subdivision of Kv equals

      : Def6: ( subdivision (n,( center_of_mass V),Kv));

      coherence

      proof

        defpred P[ Nat] means ( subdivision ($1,( center_of_mass V),Kv)) is non void Subdivision of Kv;

        

         A2: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume P[k];

          then

          reconsider P = ( subdivision (k,( center_of_mass V),Kv)) as non void Subdivision of Kv;

          

           A3: |.P.| = |.Kv.| & ( [#] P) = ( [#] Kv) by Th10, SIMPLEX0: 64;

          k in NAT by ORDINAL1:def 12;

          

          then ( subdivision ((k + 1),( center_of_mass V),Kv)) = ( subdivision (1,( center_of_mass V),( subdivision (k,( center_of_mass V),Kv)))) by SIMPLEX0: 63

          .= ( subdivision (( center_of_mass V),P)) by SIMPLEX0: 62

          .= ( BCS P) by A1, A3, Def5;

          hence thesis by Th14;

        end;

        Kv = ( subdivision ( 0 ,( center_of_mass V),Kv)) by SIMPLEX0: 61;

        then

         A4: P[ 0 qua Nat] by Th11;

        for k holds P[k] from NAT_1:sch 2( A4, A2);

        hence thesis;

      end;

    end

    theorem :: SIMPLEX1:16

    

     Th16: |.Kv.| c= ( [#] Kv) implies ( BCS ( 0 ,Kv)) = Kv

    proof

      assume |.Kv.| c= ( [#] Kv);

      

      hence ( BCS ( 0 ,Kv)) = ( subdivision ( 0 ,( center_of_mass V),Kv)) by Def6

      .= Kv by SIMPLEX0: 61;

    end;

    theorem :: SIMPLEX1:17

    

     Th17: |.Kv.| c= ( [#] Kv) implies ( BCS (1,Kv)) = ( BCS Kv)

    proof

      assume

       A1: |.Kv.| c= ( [#] Kv);

      

      hence ( BCS (1,Kv)) = ( subdivision (1,( center_of_mass V),Kv)) by Def6

      .= ( subdivision (( center_of_mass V),Kv)) by SIMPLEX0: 62

      .= ( BCS Kv) by A1, Def5;

    end;

    theorem :: SIMPLEX1:18

    

     Th18: |.Kv.| c= ( [#] Kv) implies ( [#] ( BCS (n,Kv))) = ( [#] Kv)

    proof

      assume |.Kv.| c= ( [#] Kv);

      then ( BCS (n,Kv)) = ( subdivision (n,( center_of_mass V),Kv)) by Def6;

      hence thesis by SIMPLEX0: 64;

    end;

    theorem :: SIMPLEX1:19

     |.Kv.| c= ( [#] Kv) implies |.( BCS (n,Kv)).| = |.Kv.| by Th10;

    theorem :: SIMPLEX1:20

    

     Th20: |.Kv.| c= ( [#] Kv) implies ( BCS ((n + 1),Kv)) = ( BCS ( BCS (n,Kv)))

    proof

      

       A1: |.( BCS (n,Kv)).| = |.Kv.| by Th10;

      assume

       A2: |.Kv.| c= ( [#] Kv);

      then

       A3: ( [#] ( BCS (n,Kv))) = ( [#] Kv) by Th18;

      n in NAT by ORDINAL1:def 12;

      

      then ( subdivision ((1 + n),( center_of_mass V),Kv)) = ( subdivision (1,( center_of_mass V),( subdivision (n,( center_of_mass V),Kv)))) by SIMPLEX0: 63

      .= ( subdivision (1,( center_of_mass V),( BCS (n,Kv)))) by A2, Def6

      .= ( BCS (1,( BCS (n,Kv)))) by A2, A3, A1, Def6

      .= ( BCS ( BCS (n,Kv))) by A2, A3, A1, Th17;

      hence thesis by A2, Def6;

    end;

    theorem :: SIMPLEX1:21

    

     Th21: |.Kv.| c= ( [#] Kv) & ( degree Kv) <= 0 implies the TopStruct of Kv = ( BCS Kv)

    proof

      reconsider o = 1 as ExtReal;

      assume that

       A1: |.Kv.| c= ( [#] Kv) and

       A2: ( degree Kv) <= 0 ;

      set B = ( center_of_mass V), BC = ( BCS Kv);

      

       A3: BC = ( subdivision (( center_of_mass V),Kv)) by A1, Def5;

      then

       A4: ( [#] BC) = ( [#] Kv) by SIMPLEX0:def 20;

      

       A5: ( dom B) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

      

       A6: ( 0 + o) = ( 0 + 1) & (( degree Kv) + o) <= ( 0 + o) by A2, XXREAL_3: 35, XXREAL_3:def 2;

      

       A7: the topology of BC c= the topology of Kv

      proof

        let x be object;

        assume x in the topology of BC;

        then

        reconsider X = x as Simplex of BC by PRE_TOPC:def 2;

        reconsider X1 = X as Subset of Kv by A4;

        consider S be c=-linear finite simplex-like Subset-Family of Kv such that

         A8: X = (B .: S) by A3, SIMPLEX0:def 20;

        

         A9: (B .: S) = (B .: (S /\ ( dom B))) by RELAT_1: 112;

        per cases ;

          suppose X is empty;

          then X1 is simplex-like;

          hence thesis;

        end;

          suppose

           A10: X is non empty;

          then S is non empty by A8;

          then ( union S) in S by SIMPLEX0: 9;

          then

          reconsider U = ( union S) as Simplex of Kv by TOPS_2:def 1;

          

           A11: U is non empty

          proof

            assume

             A12: U is empty;

            (S /\ ( dom B)) is empty

            proof

              assume (S /\ ( dom B)) is non empty;

              then

              consider y be object such that

               A13: y in (S /\ ( dom B));

              reconsider y as set by TARSKI: 1;

              y in S by A13, XBOOLE_0:def 4;

              then

               A14: y c= U by ZFMISC_1: 74;

              y <> {} by A13, ZFMISC_1: 56;

              hence contradiction by A12, A14;

            end;

            hence contradiction by A8, A9, A10;

          end;

          then

           A15: ( @ U) in ( dom B) by A5, ZFMISC_1: 56;

          ( card U) <= (( degree Kv) + 1) by SIMPLEX0: 24;

          then

           A16: ( card U) <= 1 by A6, XXREAL_0: 2;

          ( card U) >= 1 by A11, NAT_1: 14;

          then

           A17: ( card U) = 1 by A16, XXREAL_0: 1;

          then

          consider u be object such that

           A18: {u} = ( @ U) by CARD_2: 42;

          u in {u} by TARSKI:def 1;

          then

          reconsider u as Element of V by A18;

          

           A19: (S /\ ( dom B)) c= {U}

          proof

            let y be object;

            reconsider yy = y as set by TARSKI: 1;

            assume

             A20: y in (S /\ ( dom B));

            then y in S by XBOOLE_0:def 4;

            then

             A21: yy c= U by ZFMISC_1: 74;

            y <> {} by A20, ZFMISC_1: 56;

            then y = U by A18, A21, ZFMISC_1: 33;

            hence thesis by TARSKI:def 1;

          end;

          (S /\ ( dom B)) is non empty by A8, A9, A10;

          then (S /\ ( dom B)) = {U} by A19, ZFMISC_1: 33;

          

          then X = ( Im (B,U)) by A8, A9, RELAT_1:def 16

          .= {(B . U)} by A15, FUNCT_1: 59

          .= {((1 / 1) * ( Sum {u}))} by A17, A18, RLAFFIN2:def 2

          .= {( Sum {u})} by RLVECT_1:def 8

          .= U by A18, RLVECT_2: 9;

          hence thesis by PRE_TOPC:def 2;

        end;

      end;

      the topology of Kv c= the topology of BC

      proof

        let x be object;

        assume x in the topology of Kv;

        then

        reconsider X = x as Simplex of Kv by PRE_TOPC:def 2;

        reconsider X1 = X as Subset of BC by A4;

        per cases ;

          suppose X is empty;

          then X1 is simplex-like;

          hence thesis;

        end;

          suppose

           A22: X is non empty;

          for Y be Subset of Kv st Y in {X} holds Y is simplex-like by TARSKI:def 1;

          then

          reconsider XX = {X} as finite simplex-like Subset-Family of Kv by TOPS_2:def 1;

          now

            let x, y;

            assume that

             A23: x in XX and

             A24: y in XX;

            x = X by A23, TARSKI:def 1;

            hence (x,y) are_c=-comparable by A24, TARSKI:def 1;

          end;

          then

           A25: XX is c=-linear;

          ( card X) <= (( degree Kv) + 1) by SIMPLEX0: 24;

          then

           A26: ( card X) <= 1 by A6, XXREAL_0: 2;

          ( card X) >= 1 by A22, NAT_1: 14;

          then

           A27: ( card X) = 1 by A26, XXREAL_0: 1;

          then

          consider u be object such that

           A28: ( @ X) = {u} by CARD_2: 42;

          

           A29: ( @ X) in ( dom B) by A5, A22, ZFMISC_1: 56;

          u in {u} by TARSKI:def 1;

          then

          reconsider u as Element of V by A28;

          (B .: XX) = ( Im (B,X)) by RELAT_1:def 16

          .= {(B . X)} by A29, FUNCT_1: 59

          .= {((1 / 1) * ( Sum {u}))} by A27, A28, RLAFFIN2:def 2

          .= {( Sum {u})} by RLVECT_1:def 8

          .= X1 by A28, RLVECT_2: 9;

          then X1 is simplex-like by A3, A25, SIMPLEX0:def 20;

          hence thesis;

        end;

      end;

      hence thesis by A3, A4, A7, XBOOLE_0:def 10;

    end;

    theorem :: SIMPLEX1:22

    

     Th22: n > 0 & |.Kv.| c= ( [#] Kv) & ( degree Kv) <= 0 implies the TopStruct of Kv = ( BCS (n,Kv))

    proof

      assume that

       A1: n > 0 and

       A2: |.Kv.| c= ( [#] Kv) and

       A3: ( degree Kv) <= 0 ;

      defpred P[ Nat] means $1 > 0 implies the TopStruct of Kv = ( BCS ($1,Kv)) & ( degree ( BCS ($1,Kv))) <= 0 ;

      

       A4: for n st P[n] holds P[(n + 1)]

      proof

         not {} in ( dom ( center_of_mass V)) by ZFMISC_1: 56;

        then

         A5: ( dom ( center_of_mass V)) is with_non-empty_elements;

        let n such that

         A6: P[n];

        assume (n + 1) > 0 ;

        per cases ;

          suppose

           A7: n = 0 ;

          

           A8: ( degree ( subdivision (( center_of_mass V),Kv))) <= ( degree Kv) by A5, SIMPLEX0: 52;

          ( BCS ((n + 1),Kv)) = ( BCS Kv) by A2, A7, Th17;

          hence thesis by A2, A3, A8, Def5, Th21;

        end;

          suppose

           A9: n > 0 ;

          

           A10: |.Kv.| = |.( BCS (n,Kv)).| by Th10;

          ( [#] Kv) = ( [#] ( BCS (n,Kv))) by A6, A9;

          then ( BCS (n,Kv)) = ( BCS ( BCS (n,Kv))) by A2, A6, A9, A10, Th21;

          hence thesis by A2, A6, A9, Th20;

        end;

      end;

      

       A11: P[ 0 qua Nat];

      for n holds P[n] from NAT_1:sch 2( A11, A4);

      hence thesis by A1;

    end;

    theorem :: SIMPLEX1:23

    

     Th23: for Sv be non void SubSimplicialComplex of Kv st |.Kv.| c= ( [#] Kv) & |.Sv.| c= ( [#] Sv) holds ( BCS (n,Sv)) is SubSimplicialComplex of ( BCS (n,Kv))

    proof

      let S be non void SubSimplicialComplex of Kv;

      assume |.Kv.| c= ( [#] Kv) & |.S.| c= ( [#] S);

      then ( BCS (n,S)) = ( subdivision (n,( center_of_mass V),S)) & ( BCS (n,Kv)) = ( subdivision (n,( center_of_mass V),Kv)) by Def6;

      hence thesis by SIMPLEX0: 65;

    end;

    theorem :: SIMPLEX1:24

    

     Th24: |.Kv.| c= ( [#] Kv) implies ( Vertices Kv) c= ( Vertices ( BCS (n,Kv)))

    proof

      set S = ( Skeleton_of (Kv, 0 ));

      assume

       A1: |.Kv.| c= ( [#] Kv);

      per cases ;

        suppose n = 0 ;

        hence thesis by A1, Th16;

      end;

        suppose

         A2: n > 0 ;

        the topology of S c= the topology of Kv by SIMPLEX0:def 13;

        then |.S.| c= |.Kv.| by Th4;

        then

         A3: |.S.| c= ( [#] S) by A1;

        then ( degree S) <= 0 & ( BCS (n,S)) is SubSimplicialComplex of ( BCS (n,Kv)) by A1, Th23, SIMPLEX0: 44;

        then S is SubSimplicialComplex of ( BCS (n,Kv)) by A2, A3, Th22;

        then

         A4: ( Vertices S) c= ( Vertices ( BCS (n,Kv))) by SIMPLEX0: 31;

        let x be object;

        assume

         A5: x in ( Vertices Kv);

        then

        reconsider v = x as Element of Kv;

        v is vertex-like by A5, SIMPLEX0:def 4;

        then

        consider A be Subset of Kv such that

         A6: A is simplex-like and

         A7: v in A;

        reconsider vv = {v} as Subset of Kv by A7, ZFMISC_1: 31;

         {v} c= A by A7, ZFMISC_1: 31;

        then vv is simplex-like by A6, MATROID0: 1;

        then

         A8: vv in the topology of Kv;

        ( card vv) = 1 & ( card 1) = 1 by CARD_1: 30;

        then vv in ( the_subsets_with_limited_card (1,the topology of Kv)) by A8, SIMPLEX0:def 2;

        then vv in the topology of S by SIMPLEX0: 2;

        then

        reconsider vv as Simplex of S by PRE_TOPC:def 2;

        

         A9: v in vv by TARSKI:def 1;

        reconsider v as Element of S;

        v is vertex-like by A9;

        then v in ( Vertices S) by SIMPLEX0:def 4;

        hence thesis by A4;

      end;

    end;

    registration

      let n, V;

      let K be non void total SimplicialComplex of V;

      cluster ( BCS (n,K)) -> total;

      coherence

      proof

        

         A1: ( [#] K) = ( [#] V) by SIMPLEX0:def 10;

        then |.K.| c= ( [#] K);

        then ( [#] ( BCS (n,K))) = ( [#] V) by A1, Th18;

        hence thesis;

      end;

    end

    registration

      let n, V;

      let K be non void finite-vertices total SimplicialComplex of V;

      cluster ( BCS (n,K)) -> finite-vertices;

      coherence

      proof

        defpred P[ Nat] means ( BCS ($1,K)) is finite-vertices;

        ( [#] K) = ( [#] V) by SIMPLEX0:def 10;

        then

         A1: |.K.| c= ( [#] K);

        

         A2: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A3: P[n];

          ( [#] ( BCS (n,K))) = ( [#] V) by SIMPLEX0:def 10;

          then

           A4: |.( BCS (n,K)).| c= ( [#] ( BCS (n,K)));

          ( BCS ((n + 1),K)) = ( BCS ( BCS (n,K))) by A1, Th20

          .= ( subdivision (( center_of_mass V),( BCS (n,K)))) by A4, Def5;

          hence thesis by A3;

        end;

        

         A5: P[ 0 qua Nat] by A1, Th16;

        for n holds P[n] from NAT_1:sch 2( A5, A2);

        hence thesis;

      end;

    end

    begin

    definition

      let V;

      let K be SimplicialComplexStr of V;

      :: SIMPLEX1:def7

      attr K is affinely-independent means

      : Def7: for A be Subset of K st A is simplex-like holds ( @ A) is affinely-independent;

    end

    definition

      let RLS, Kr;

      :: SIMPLEX1:def8

      attr Kr is simplex-join-closed means

      : Def8: for A,B be Subset of Kr st A is simplex-like & B is simplex-like holds (( conv ( @ A)) /\ ( conv ( @ B))) = ( conv ( @ (A /\ B)));

    end

    registration

      let V;

      cluster empty-membered -> affinely-independent for SimplicialComplexStr of V;

      coherence

      proof

        let K be SimplicialComplexStr of V;

        assume K is empty-membered;

        then

         A1: the topology of K is empty-membered;

        let A be Subset of K;

        assume A is simplex-like;

        then A in the topology of K;

        then A is empty by A1;

        hence thesis;

      end;

      let F be affinely-independent Subset-Family of V;

      cluster ( Complex_of F) -> affinely-independent;

      coherence

      proof

        let A be Subset of ( Complex_of F);

        assume A is simplex-like;

        then A in ( subset-closed_closure_of F);

        then

        consider x such that

         A2: A c= x and

         A3: x in F by SIMPLEX0: 2;

        x is affinely-independent Subset of V by A3, RLAFFIN1:def 5;

        hence thesis by A2, RLAFFIN1: 43;

      end;

    end

    registration

      let RLS;

      cluster empty-membered -> simplex-join-closed for SimplicialComplexStr of RLS;

      coherence

      proof

        let K be SimplicialComplexStr of RLS;

        assume K is empty-membered;

        then

         A1: the topology of K is empty-membered;

        let A,B be Subset of K;

        assume that

         A2: A is simplex-like and

         A3: B is simplex-like;

        A in the topology of K by A2;

        then

         A4: A is empty by A1;

        B in the topology of K by A3;

        then B is empty by A1;

        hence thesis by A4;

      end;

    end

    registration

      let V;

      let I be affinely-independent Subset of V;

      cluster ( Complex_of {I}) -> simplex-join-closed;

      coherence

      proof

        set C = ( Complex_of {I});

        let A,B be Subset of C;

        assume that

         A1: A is simplex-like and

         A2: B is simplex-like;

        

         A3: the topology of C = ( bool I) by SIMPLEX0: 4;

        

         A4: B in the topology of C by A2;

        

         A5: (A /\ B) c= A by XBOOLE_1: 17;

        

         A6: ( @ A) is affinely-independent by A1, Def7;

        

         A7: ( conv ( @ B)) c= ( Affin ( @ B)) by RLAFFIN1: 65;

        

         A8: ( conv ( @ A)) c= ( Affin ( @ A)) by RLAFFIN1: 65;

        

         A9: A in the topology of C by A1;

        then

         A10: ( Affin ( @ A)) c= ( Affin I) by A3, RLAFFIN1: 52;

        

         A11: ( @ (A /\ B)) is affinely-independent by A1, Def7;

        thus (( conv ( @ A)) /\ ( conv ( @ B))) c= ( conv ( @ (A /\ B)))

        proof

          let x be object;

          set IAB = (I \ ( @ (A /\ B)));

          

           A12: ( @ (A /\ B)) = (I /\ ( @ (A /\ B))) by A3, A5, A9, XBOOLE_1: 1, XBOOLE_1: 28

          .= (I \ IAB) by XBOOLE_1: 48;

          assume

           A13: x in (( conv ( @ A)) /\ ( conv ( @ B)));

          then

           A14: x in ( conv ( @ A)) by XBOOLE_0:def 4;

          then

           A15: (x |-- ( @ A)) = (x |-- I) by A3, A8, A9, RLAFFIN1: 77;

          x in ( conv ( @ B)) by A13, XBOOLE_0:def 4;

          then

           A16: (x |-- ( @ B)) = (x |-- I) by A3, A4, A7, RLAFFIN1: 77;

          

           A17: ( Carrier (x |-- ( @ A))) c= A & ( Carrier (x |-- ( @ B))) c= B by RLVECT_2:def 6;

          

           A18: for y st y in IAB holds ((x |-- I) . y) = 0

          proof

            let y;

            assume

             A19: y in IAB;

            then not y in (A /\ B) by XBOOLE_0:def 5;

            then not y in ( Carrier (x |-- ( @ A))) or not y in ( Carrier (x |-- ( @ B))) by A17, XBOOLE_0:def 4;

            hence thesis by A15, A16, A19;

          end;

          

           A20: x in ( Affin ( @ A)) by A8, A14;

           A21:

          now

            let v be Element of V;

            assume v in ( @ (A /\ B));

             0 <= ((x |-- ( @ A)) . v) by A6, A14, RLAFFIN1: 71;

            hence 0 <= ((x |-- ( @ (A /\ B))) . v) by A10, A12, A15, A18, A20, RLAFFIN1: 75;

          end;

          x in ( Affin ( @ (A /\ B))) by A10, A12, A18, A20, RLAFFIN1: 75;

          hence x in ( conv ( @ (A /\ B))) by A11, A21, RLAFFIN1: 73;

        end;

        ( conv ( @ (A /\ B))) c= ( conv ( @ A)) & ( conv ( @ (A /\ B))) c= ( conv ( @ B)) by RLTOPSP1: 20, XBOOLE_1: 17;

        hence thesis by XBOOLE_1: 19;

      end;

    end

    registration

      let V;

      cluster 1 -element affinely-independent for Subset of V;

      existence

      proof

        take { the Element of V};

        thus thesis;

      end;

    end

    registration

      let V;

      cluster with_non-empty_element finite-vertices affinely-independent simplex-join-closed total for SimplicialComplex of V;

      existence

      proof

        set v = the Element of V;

        take ( Complex_of { {v}});

        thus thesis;

      end;

    end

    registration

      let V;

      let K be affinely-independent SimplicialComplexStr of V;

      cluster -> affinely-independent for SubSimplicialComplex of K;

      coherence

      proof

        let S be SubSimplicialComplex of K;

        let A be Subset of S;

        assume A is simplex-like;

        then

         A1: A in the topology of S;

        

         A2: the topology of S c= the topology of K by SIMPLEX0:def 13;

        then A in the topology of K by A1;

        then

        reconsider A1 = A as Subset of K;

        A1 is simplex-like by A1, A2;

        then ( @ A1) is affinely-independent by Def7;

        hence thesis;

      end;

    end

    registration

      let V;

      let K be simplex-join-closed SimplicialComplexStr of V;

      cluster -> simplex-join-closed for SubSimplicialComplex of K;

      coherence

      proof

        let S be SubSimplicialComplex of K;

        

         A1: the topology of S c= the topology of K by SIMPLEX0:def 13;

        let A,B be Subset of S;

        assume that

         A2: A is simplex-like and

         A3: B is simplex-like;

        

         A4: A in the topology of S by A2;

        then

         A5: A in the topology of K by A1;

        

         A6: B in the topology of S by A3;

        then B in the topology of K by A1;

        then

        reconsider A1 = A, B1 = B as Subset of K by A5;

        

         A7: A1 is simplex-like by A1, A4;

        B1 is simplex-like by A1, A6;

        then (( conv ( @ A1)) /\ ( conv ( @ B1))) = ( conv ( @ (A1 /\ B1))) by A7, Def8;

        hence thesis;

      end;

    end

    theorem :: SIMPLEX1:25

    

     Th25: for K be subset-closed SimplicialComplexStr of V holds K is simplex-join-closed iff for A,B be Subset of K st A is simplex-like & B is simplex-like & ( Int ( @ A)) meets ( Int ( @ B)) holds A = B

    proof

      let K be subset-closed SimplicialComplexStr of V;

      hereby

        assume

         A1: K is simplex-join-closed;

        let A,B be Subset of K such that

         A2: A is simplex-like & B is simplex-like and

         A3: ( Int ( @ A)) meets ( Int ( @ B));

        

         A4: (( conv ( @ A)) /\ ( conv ( @ B))) = ( conv ( @ (A /\ B))) by A1, A2;

        assume A <> B;

        then

         A5: (A /\ B) <> A or (A /\ B) <> B;

        

         A6: (A /\ B) c= A & (A /\ B) c= B by XBOOLE_1: 17;

        consider x be object such that

         A7: x in ( Int ( @ A)) and

         A8: x in ( Int ( @ B)) by A3, XBOOLE_0: 3;

        ( Int ( @ A)) c= ( conv ( @ A)) & ( Int ( @ B)) c= ( conv ( @ B)) by RLAFFIN2: 5;

        then

         A9: x in (( conv ( @ A)) /\ ( conv ( @ B))) by A7, A8, XBOOLE_0:def 4;

        per cases by A5, A6;

          suppose (A /\ B) c< A;

          then ( conv ( @ (A /\ B))) misses ( Int ( @ A)) by RLAFFIN2: 7;

          hence contradiction by A4, A7, A9, XBOOLE_0: 3;

        end;

          suppose (A /\ B) c< B;

          then ( conv ( @ (A /\ B))) misses ( Int ( @ B)) by RLAFFIN2: 7;

          hence contradiction by A4, A8, A9, XBOOLE_0: 3;

        end;

      end;

      assume

       A10: for A,B be Subset of K st A is simplex-like & B is simplex-like & ( Int ( @ A)) meets ( Int ( @ B)) holds A = B;

      let A,B be Subset of K such that

       A11: A is simplex-like and

       A12: B is simplex-like;

      

       A13: (( conv ( @ A)) /\ ( conv ( @ B))) c= ( conv ( @ (A /\ B)))

      proof

        let x be object;

        

         A14: ( the_family_of K) is subset-closed;

        assume

         A15: x in (( conv ( @ A)) /\ ( conv ( @ B)));

        then x in ( conv ( @ A)) by XBOOLE_0:def 4;

        then x in ( union { ( Int a) where a be Subset of V : a c= ( @ A) }) by RLAFFIN2: 8;

        then

        consider Ia be set such that

         A16: x in Ia and

         A17: Ia in { ( Int a) where a be Subset of V : a c= ( @ A) } by TARSKI:def 4;

        consider a be Subset of V such that

         A18: Ia = ( Int a) and

         A19: a c= ( @ A) by A17;

        x in ( conv ( @ B)) by A15, XBOOLE_0:def 4;

        then x in ( union { ( Int b) where b be Subset of V : b c= ( @ B) }) by RLAFFIN2: 8;

        then

        consider Ib be set such that

         A20: x in Ib and

         A21: Ib in { ( Int b) where b be Subset of V : b c= ( @ B) } by TARSKI:def 4;

        consider b be Subset of V such that

         A22: Ib = ( Int b) and

         A23: b c= ( @ B) by A21;

        reconsider a1 = a, b1 = b as Subset of K by A19, A23, XBOOLE_1: 1;

        A in the topology of K by A11;

        then a1 in the topology of K by A14, A19, CLASSES1:def 1;

        then

         A24: a1 is simplex-like;

        B in the topology of K by A12;

        then b1 in the topology of K by A14, A23, CLASSES1:def 1;

        then

         A25: b1 is simplex-like;

        ( Int ( @ a1)) meets ( Int ( @ b1)) by A16, A18, A20, A22, XBOOLE_0: 3;

        then a1 = b1 by A10, A24, A25;

        then a c= ( @ (A /\ B)) by A19, A23, XBOOLE_1: 19;

        then

         A26: ( conv a) c= ( conv ( @ (A /\ B))) by RLAFFIN1: 3;

        x in ( conv a) by A16, A18, RLAFFIN2:def 1;

        hence thesis by A26;

      end;

      ( conv ( @ (A /\ B))) c= ( conv ( @ A)) & ( conv ( @ (A /\ B))) c= ( conv ( @ B)) by RLAFFIN1: 3, XBOOLE_1: 17;

      then ( conv ( @ (A /\ B))) c= (( conv ( @ A)) /\ ( conv ( @ B))) by XBOOLE_1: 19;

      hence thesis by A13;

    end;

    reserve Ks for simplex-join-closed SimplicialComplex of V,

As,Bs for Subset of Ks,

Ka for non void affinely-independent SimplicialComplex of V,

Kas for non void affinely-independent simplex-join-closed SimplicialComplex of V,

K for non void affinely-independent simplex-join-closed total SimplicialComplex of V;

    registration

      let V, Ka;

      let S be Simplex of Ka;

      cluster ( @ S) -> affinely-independent;

      coherence by Def7;

    end

    theorem :: SIMPLEX1:26

    

     Th26: As is simplex-like & Bs is simplex-like & ( Int ( @ As)) meets ( conv ( @ Bs)) implies As c= Bs

    proof

      assume that

       A1: As is simplex-like and

       A2: Bs is simplex-like and

       A3: ( Int ( @ As)) meets ( conv ( @ Bs));

      consider x be object such that

       A4: x in ( Int ( @ As)) and

       A5: x in ( conv ( @ Bs)) by A3, XBOOLE_0: 3;

      x in ( union { ( Int b) where b be Subset of V : b c= ( @ Bs) }) by A5, RLAFFIN2: 8;

      then

      consider Ib be set such that

       A6: x in Ib and

       A7: Ib in { ( Int b) where b be Subset of V : b c= ( @ Bs) } by TARSKI:def 4;

      consider b be Subset of V such that

       A8: Ib = ( Int b) and

       A9: b c= ( @ Bs) by A7;

      reconsider b1 = b as Subset of Ks by A9, XBOOLE_1: 1;

      As in the topology of Ks by A1;

      then Ks is non void by PENCIL_1:def 4;

      then

       A10: b1 is simplex-like by A2, A9, MATROID0: 1;

      ( Int ( @ As)) meets ( Int ( @ b1)) by A4, A6, A8, XBOOLE_0: 3;

      hence thesis by A1, A9, A10, Th25;

    end;

    theorem :: SIMPLEX1:27

    As is simplex-like & ( @ As) is affinely-independent & Bs is simplex-like implies (( Int ( @ As)) c= ( conv ( @ Bs)) iff As c= Bs)

    proof

      assume that

       A1: As is simplex-like and

       A2: ( @ As) is affinely-independent and

       A3: Bs is simplex-like;

      As in the topology of Ks by A1;

      then

       A4: Ks is non void by PENCIL_1:def 4;

      per cases ;

        suppose

         A5: As is empty;

        thus thesis by A5;

      end;

        suppose As is non empty;

        then ( Int ( @ As)) is non empty by A1, A2, A4, RLAFFIN2: 20;

        then

        consider x be object such that

         A6: x in ( Int ( @ As));

        hereby

          assume ( Int ( @ As)) c= ( conv ( @ Bs));

          then x in ( conv ( @ Bs)) by A6;

          then x in ( union { ( Int b) where b be Subset of V : b c= ( @ Bs) }) by RLAFFIN2: 8;

          then

          consider Ib be set such that

           A7: x in Ib and

           A8: Ib in { ( Int b) where b be Subset of V : b c= ( @ Bs) } by TARSKI:def 4;

          consider b be Subset of V such that

           A9: Ib = ( Int b) and

           A10: b c= ( @ Bs) by A8;

          reconsider b1 = b as Subset of Ks by A10, XBOOLE_1: 1;

          

           A11: b1 is simplex-like by A3, A4, A10, MATROID0: 1;

          ( Int ( @ As)) meets ( Int ( @ b1)) by A6, A7, A9, XBOOLE_0: 3;

          hence As c= Bs by A1, A10, A11, Th25;

        end;

        assume As c= Bs;

        then ( Int ( @ As)) c= ( conv ( @ As)) & ( conv ( @ As)) c= ( conv ( @ Bs)) by RLAFFIN1: 3, RLAFFIN2: 5;

        hence thesis;

      end;

    end;

    theorem :: SIMPLEX1:28

    

     Th28: |.Ka.| c= ( [#] Ka) implies ( BCS Ka) is affinely-independent

    proof

      set P = ( BCS Ka), B = ( center_of_mass V);

      assume |.Ka.| c= ( [#] Ka);

      then

       A1: P = ( subdivision (B,Ka)) by Def5;

      let A be Subset of P;

      assume A is simplex-like;

      then

      consider S be c=-linear finite simplex-like Subset-Family of Ka such that

       A2: A = (B .: S) by A1, SIMPLEX0:def 20;

      per cases ;

        suppose S is empty;

        then A = {} by A2;

        hence thesis;

      end;

        suppose

         A3: S is non empty;

        S c= ( bool ( union S)) & ( bool ( @ ( union S))) c= ( bool the carrier of V) by ZFMISC_1: 67, ZFMISC_1: 82;

        then

        reconsider s = S as c=-linear finite Subset-Family of V by XBOOLE_1: 1;

        ( union S) in S by A3, SIMPLEX0: 9;

        then ( union S) is simplex-like by TOPS_2:def 1;

        then ( @ ( union S)) is affinely-independent;

        then ( union s) is affinely-independent;

        hence thesis by A2, RLAFFIN2: 29;

      end;

    end;

    registration

      let V;

      let Ka be non void affinely-independent total SimplicialComplex of V;

      cluster ( BCS Ka) -> affinely-independent;

      coherence

      proof

        ( [#] Ka) = the carrier of V by SIMPLEX0:def 10;

        then |.Ka.| c= ( [#] Ka);

        hence thesis by Th28;

      end;

      let n;

      cluster ( BCS (n,Ka)) -> affinely-independent;

      coherence

      proof

        defpred P[ Nat] means ( BCS ($1,Ka)) is affinely-independent;

        ( [#] Ka) = ( [#] V) by SIMPLEX0:def 10;

        then

         A1: |.Ka.| c= ( [#] Ka);

        

         A2: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A3: P[n];

          ( BCS ((n + 1),Ka)) = ( BCS ( BCS (n,Ka))) by A1, Th20;

          hence thesis by A3;

        end;

        

         A4: P[ 0 qua Nat] by A1, Th16;

        for n holds P[n] from NAT_1:sch 2( A4, A2);

        hence thesis;

      end;

    end

    registration

      let V, Kas;

      cluster (( center_of_mass V) | the topology of Kas) -> one-to-one;

      coherence

      proof

        now

          set B = ( center_of_mass V), T = the topology of Kas;

          let x1,x2 be object;

          set BT = (B | T);

          assume that

           A1: x1 in ( dom BT) and

           A2: x2 in ( dom BT) and

           A3: (BT . x1) = (BT . x2);

          

           A4: (BT . x1) = (B . x1) & (BT . x2) = (B . x2) by A1, A2, FUNCT_1: 47;

          ( dom BT) = (( dom B) /\ T) by RELAT_1: 61;

          then x1 in T & x2 in T by A1, A2, XBOOLE_0:def 4;

          then

          reconsider A1 = x1, A2 = x2 as Simplex of Kas by PRE_TOPC:def 2;

          A1 is non empty by A1, ZFMISC_1: 56;

          then

           A5: (B . A1) in ( conv ( @ A1)) by RLAFFIN2: 16;

          A2 is non empty by A2, ZFMISC_1: 56;

          then (B . A2) in ( conv ( @ A2)) by RLAFFIN2: 16;

          then

           A6: (B . A1) in (( conv ( @ A1)) /\ ( conv ( @ A2))) by A3, A4, A5, XBOOLE_0:def 4;

          

           A7: (( conv ( @ A1)) /\ ( conv ( @ A2))) = ( conv ( @ (A1 /\ A2))) & ( conv ( @ (A1 /\ A2))) c= ( Affin ( @ (A1 /\ A2))) by Def8, RLAFFIN1: 65;

          then (A1 /\ A2) = A1 by A6, RLAFFIN2: 21, XBOOLE_1: 17;

          hence x1 = x2 by A3, A4, A6, A7, RLAFFIN2: 21, XBOOLE_1: 17;

        end;

        hence thesis by FUNCT_1:def 4;

      end;

    end

    theorem :: SIMPLEX1:29

    

     Th29: |.Kas.| c= ( [#] Kas) implies ( BCS Kas) is simplex-join-closed

    proof

      set B = ( center_of_mass V);

      set BC = ( BCS Kas);

      defpred P[ Nat] means for S1,S2 be c=-linear finite simplex-like Subset-Family of Kas holds for A1,A2 be Simplex of BC st A1 = (B .: S1) & A2 = (B .: S2) & ( card ( union S1)) <= $1 & ( card ( union S2)) <= $1 & ( Int ( @ A1)) meets ( Int ( @ A2)) holds A1 = A2;

      assume

       A1: |.Kas.| c= ( [#] Kas);

      then

       A2: BC = ( subdivision (B,Kas)) by Def5;

      

       A3: BC is affinely-independent by A1, Th28;

      

       A4: ( dom B) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

      

       A5: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A6: P[n];

        let S1,S2 be c=-linear finite simplex-like Subset-Family of Kas;

        let A1,A2 be Simplex of BC such that

         A7: A1 = (B .: S1) and

         A8: A2 = (B .: S2) and

         A9: ( card ( union S1)) <= (n + 1) and ( card ( union S2)) <= (n + 1) and

         A10: ( Int ( @ A1)) meets ( Int ( @ A2));

        

         A11: ( union S2) in S2 or S2 is empty by SIMPLEX0: 9;

        then

         A12: ( union S2) is simplex-like by TOPS_2:def 1, ZFMISC_1: 2;

        set U = ( union S1);

        S2 c= ( bool ( union S2)) & ( bool ( @ ( union S2))) c= ( bool the carrier of V) by ZFMISC_1: 67, ZFMISC_1: 82;

        then

         A13: S2 is Subset-Family of V by XBOOLE_1: 1;

        

         A14: ( union S1) in S1 or S1 is empty by SIMPLEX0: 9;

        then

         A15: ( union S1) is simplex-like by TOPS_2:def 1, ZFMISC_1: 2;

        S1 c= ( bool ( union S1)) & ( bool ( @ ( union S1))) c= ( bool the carrier of V) by ZFMISC_1: 67, ZFMISC_1: 82;

        then

         A16: S1 is Subset-Family of V by XBOOLE_1: 1;

        then

         A17: ( Int (B .: S1)) c= ( Int ( @ ( union S1))) by A15, RLAFFIN2: 30;

        ( Int ( @ ( union S1))) meets ( Int (B .: S2)) by A7, A8, A10, A15, A16, RLAFFIN2: 30, XBOOLE_1: 63;

        then ( Int ( @ ( union S1))) meets ( Int ( @ ( union S2))) by A13, A12, RLAFFIN2: 30, XBOOLE_1: 63;

        then

         A18: ( union S1) = ( union S2) by A12, A15, Th25;

        per cases by A9, NAT_1: 8;

          suppose ( card ( union S1)) <= n;

          hence thesis by A6, A7, A8, A10, A18;

        end;

          suppose

           A19: ( card ( union S1)) = (n + 1);

          then

           A20: ( @ ( union S1)) is non empty;

          then

           A21: ( union S1) in ( dom B) by A4, ZFMISC_1: 56;

          then

           A22: (B . ( union S1)) in ( @ A1) by A7, A14, A19, FUNCT_1:def 6, ZFMISC_1: 2;

          then

          reconsider Bu = (B . ( union S1)) as Element of V;

          

           A23: {Bu} c= ( @ A1) by A22, ZFMISC_1: 31;

          

           A24: (B . ( union S1)) in ( @ A2) by A8, A11, A18, A19, A21, FUNCT_1:def 6, ZFMISC_1: 2;

          then

           A25: {Bu} c= ( @ A2) by ZFMISC_1: 31;

          

           A26: Bu in {Bu} by ZFMISC_1: 31;

          

           A27: ( conv {Bu}) = {Bu} by RLAFFIN1: 1;

          consider x be object such that

           A28: x in ( Int ( @ A1)) and

           A29: x in ( Int ( @ A2)) by A10, XBOOLE_0: 3;

          reconsider x as Element of V by A28;

          per cases ;

            suppose A1 = {Bu} & A2 = {Bu};

            hence thesis;

          end;

            suppose

             A30: A1 = {Bu} & A2 <> {Bu};

            then {Bu} c< ( @ A2) & ( Int ( @ A1)) = ( @ A1) by A25, RLAFFIN2: 6;

            hence thesis by A27, A28, A29, A30, RLAFFIN2:def 1;

          end;

            suppose

             A31: A1 <> {Bu} & A2 = {Bu};

            then {Bu} c< ( @ A1) & ( Int ( @ A2)) = ( @ A2) by A23, RLAFFIN2: 6;

            hence thesis by A27, A28, A29, A31, RLAFFIN2:def 1;

          end;

            suppose A1 <> {Bu} & A2 <> {Bu};

            then {Bu} c< ( @ A1) by A23;

            then

             A32: Bu <> x by A26, A27, A28, RLAFFIN2:def 1;

            (S1 \ {U}) c= S1 & (S2 \ {U}) c= S2 by XBOOLE_1: 36;

            then

            reconsider s1u = (S1 \ {U}), s2u = (S2 \ {U}) as c=-linear finite simplex-like Subset-Family of Kas by TOPS_2: 11;

            

             A33: S1 c= the topology of Kas

            proof

              let x be object;

              assume

               A34: x in S1;

              then

              reconsider A = x as Subset of Kas;

              A is simplex-like by A34, TOPS_2:def 1;

              hence thesis;

            end;

            ( [#] Kas) c= the carrier of V by SIMPLEX0:def 9;

            then ( bool the carrier of Kas) c= ( bool the carrier of V) by ZFMISC_1: 67;

            then

            reconsider S1U = s1u, S2U = s2u as Subset-Family of V by XBOOLE_1: 1;

            set Bu1 = (x |-- ( @ A1));

            set Bu2 = (x |-- ( @ A2));

            set BT = (B | the topology of Kas);

            

             A35: (S1 \ {U}) c= S1 by XBOOLE_1: 36;

            

             A36: {U} c= S1 by A14, A19, ZFMISC_1: 2, ZFMISC_1: 31;

            

             A37: ( union s2u) c= U by A18, XBOOLE_1: 36, ZFMISC_1: 77;

            ( union s2u) <> U

            proof

              assume

               A38: ( union s2u) = U;

              then ( union s2u) in s2u by A20, SIMPLEX0: 9, ZFMISC_1: 2;

              hence contradiction by A38, ZFMISC_1: 56;

            end;

            then

             A39: ( union s2u) c< U by A37;

            then

            consider xS2U be object such that

             A40: xS2U in ( @ U) and

             A41: not xS2U in ( union S2U) by XBOOLE_0: 6;

            reconsider xS2U as Element of V by A40;

            ( union S2U) c= (U \ {xS2U}) by A37, A41, ZFMISC_1: 34;

            then

             A42: ( conv ( union S2U)) c= ( conv ( @ (U \ {xS2U}))) by RLAFFIN1: 3;

            

             A43: x in ( conv ( @ A1)) by A28, RLAFFIN2:def 1;

            then

             A44: (Bu1 . Bu) <= 1 by A3, RLAFFIN1: 71;

            

             A45: (Bu1 . Bu) < 1

            proof

              assume (Bu1 . Bu) >= 1;

              then (Bu1 . Bu) = 1 by A44, XXREAL_0: 1;

              hence contradiction by A3, A32, A43, RLAFFIN1: 72;

            end;

            ( conv ( @ A1)) c= ( Affin ( @ A1)) by RLAFFIN1: 65;

            then

             A46: x = ( Sum Bu1) by A3, A43, RLAFFIN1:def 7;

            then Bu in ( Carrier Bu1) by A3, A22, A28, A43, RLAFFIN1: 71, RLAFFIN2: 11;

            then

             A47: (Bu1 . Bu) <> 0 by RLVECT_2: 19;

            Bu1 is convex by A3, A43, RLAFFIN1: 71;

            then

            consider p1 be Element of V such that

             A48: p1 in ( conv (( @ A1) \ {Bu})) and

             A49: x = (((Bu1 . Bu) * Bu) + ((1 - (Bu1 . Bu)) * p1)) and (((1 / (Bu1 . Bu)) * x) + ((1 - (1 / (Bu1 . Bu))) * p1)) = Bu by A32, A46, A47, RLAFFIN2: 1;

            

             A50: p1 in ( Int (( @ A1) \ {Bu})) by A3, A22, A28, A48, A49, RLAFFIN2: 14;

            

             A51: {Bu} = ( Im (B,( union S1))) by A21, FUNCT_1: 59

            .= (B .: {( union S1)}) by RELAT_1:def 16;

            

            then

             A52: (A1 \ {Bu}) = ((BT .: S1) \ (B .: {U})) by A33, A7, RELAT_1: 129

            .= ((BT .: S1) \ (BT .: {U})) by A33, A36, RELAT_1: 129, XBOOLE_1: 1

            .= (BT .: (S1 \ {U})) by FUNCT_1: 64

            .= (B .: (S1 \ {U})) by A35, A33, RELAT_1: 129, XBOOLE_1: 1;

            then ( conv (( @ A1) \ {Bu})) c= ( conv ( union S1U)) by CONVEX1: 30, RLAFFIN2: 17;

            then

             A53: p1 in ( conv ( union S1U)) by A48;

            ( card ( union s2u)) < (n + 1) by A19, A39, CARD_2: 48;

            then

             A54: ( card ( union s2u)) <= n by NAT_1: 13;

            

             A55: ( union s1u) c= U by XBOOLE_1: 36, ZFMISC_1: 77;

            

             A56: x in ( conv ( @ A2)) by A29, RLAFFIN2:def 1;

            then

             A57: (Bu2 . Bu) <= 1 by A3, RLAFFIN1: 71;

            

             A58: (Bu2 . Bu) < 1

            proof

              assume (Bu2 . Bu) >= 1;

              then (Bu2 . Bu) = 1 by A57, XXREAL_0: 1;

              hence contradiction by A3, A32, A56, RLAFFIN1: 72;

            end;

            ( conv ( @ A2)) c= ( Affin ( @ A2)) by RLAFFIN1: 65;

            then

             A59: x = ( Sum Bu2) by A3, A56, RLAFFIN1:def 7;

            then Bu in ( Carrier Bu2) by A3, A24, A29, A56, RLAFFIN1: 71, RLAFFIN2: 11;

            then

             A60: (Bu2 . Bu) <> 0 by RLVECT_2: 19;

            Bu2 is convex by A3, A56, RLAFFIN1: 71;

            then

            consider p2 be Element of V such that

             A61: p2 in ( conv (( @ A2) \ {Bu})) and

             A62: x = (((Bu2 . Bu) * Bu) + ((1 - (Bu2 . Bu)) * p2)) and (((1 / (Bu2 . Bu)) * x) + ((1 - (1 / (Bu2 . Bu))) * p2)) = Bu by A32, A59, A60, RLAFFIN2: 1;

            

             A63: p2 in ( Int (( @ A2) \ {Bu})) by A3, A24, A29, A61, A62, RLAFFIN2: 14;

            ( @ U) is non empty finite Subset of V by A19;

            then

             A64: Bu in ( Int ( @ U)) by A15, RLAFFIN2: 20;

            then

             A65: Bu in ( conv ( @ U)) by RLAFFIN2:def 1;

            

             A66: S2 c= the topology of Kas

            proof

              let x be object;

              assume

               A67: x in S2;

              then

              reconsider A = x as Subset of Kas;

              A is simplex-like by A67, TOPS_2:def 1;

              hence thesis;

            end;

            ( union s1u) <> U

            proof

              assume

               A68: ( union s1u) = U;

              then ( union s1u) in s1u by A20, SIMPLEX0: 9, ZFMISC_1: 2;

              hence contradiction by A68, ZFMISC_1: 56;

            end;

            then

             A69: ( union s1u) c< U by A55;

            then

            consider xS1U be object such that

             A70: xS1U in ( @ U) and

             A71: not xS1U in ( union S1U) by XBOOLE_0: 6;

            reconsider xS1U as Element of V by A70;

            ( union S1U) c= (U \ {xS1U}) by A55, A71, ZFMISC_1: 34;

            then

             A72: ( conv ( union S1U)) c= ( conv ( @ (U \ {xS1U}))) by RLAFFIN1: 3;

            (U \ {xS1U}) c= U & (U \ {xS1U}) <> U by A70, ZFMISC_1: 56;

            then (U \ {xS1U}) c< U;

            then

             A73: not Bu in ( conv ( @ (U \ {xS1U}))) by A64, RLAFFIN2:def 1;

            ( card ( union s1u)) < (n + 1) by A19, A69, CARD_2: 48;

            then

             A74: ( card ( union s1u)) <= n by NAT_1: 13;

            (U \ {xS2U}) c= U & (U \ {xS2U}) <> U by A40, ZFMISC_1: 56;

            then (U \ {xS2U}) c< U;

            then

             A75: not Bu in ( conv ( @ (U \ {xS2U}))) by A64, RLAFFIN2:def 1;

            

             A76: {U} c= S2 by A11, A18, A19, ZFMISC_1: 2, ZFMISC_1: 31;

            

             A77: (S2 \ {U}) c= S2 by XBOOLE_1: 36;

            

             A78: (A2 \ {Bu}) = ((BT .: S2) \ (B .: {U})) by A66, A8, A51, RELAT_1: 129

            .= ((BT .: S2) \ (BT .: {U})) by A76, A66, RELAT_1: 129, XBOOLE_1: 1

            .= (BT .: (S2 \ {U})) by FUNCT_1: 64

            .= (B .: (S2 \ {U})) by A66, A77, RELAT_1: 129, XBOOLE_1: 1;

            then ( conv (( @ A2) \ {Bu})) c= ( conv ( union S2U)) by CONVEX1: 30, RLAFFIN2: 17;

            then

             A79: p2 in ( conv ( union S2U)) by A61;

            x in ( conv ( @ U)) by A7, A17, A28, RLAFFIN2:def 1;

            then p2 = p1 by A15, A45, A49, A58, A62, A65, A42, A53, A75, A72, A73, A79, RLAFFIN2: 2;

            then

             A80: ( Int (( @ A1) \ {Bu})) meets ( Int (( @ A2) \ {Bu})) by A50, A63, XBOOLE_0: 3;

            (( @ A1) \ {Bu}) = ( @ (A1 \ {Bu})) & (( @ A2) \ {Bu}) = ( @ (A2 \ {Bu}));

            then (A1 \ {Bu}) = (A2 \ {Bu}) by A6, A54, A52, A74, A78, A80;

            

            hence A1 = ((A2 \ {Bu}) \/ {Bu}) by A22, ZFMISC_1: 116

            .= A2 by A24, ZFMISC_1: 116;

          end;

        end;

      end;

      

       A81: P[ 0 qua Nat]

      proof

        let S1,S2 be c=-linear finite simplex-like Subset-Family of Kas;

        let A1,A2 be Simplex of BC such that

         A82: A1 = (B .: S1) and A2 = (B .: S2) and

         A83: ( card ( union S1)) <= 0 and ( card ( union S2)) <= 0 and

         A84: ( Int ( @ A1)) meets ( Int ( @ A2));

        ( Int ( @ A1)) is non empty by A84;

        then A1 is non empty;

        then

        consider y be object such that

         A85: y in A1;

        consider x be object such that

         A86: x in ( dom B) and

         A87: x in S1 and (B . x) = y by A82, A85, FUNCT_1:def 6;

        reconsider xx = x as set by TARSKI: 1;

        

         A88: x <> {} by A86, ZFMISC_1: 56;

        ( union S1) is empty by A83;

        then xx c= {} by A87, ZFMISC_1: 74;

        hence thesis by A88;

      end;

      

       A89: for n holds P[n] from NAT_1:sch 2( A81, A5);

      now

        let A1,A2 be Subset of BC;

        assume that

         A90: A1 is simplex-like and

         A91: A2 is simplex-like and

         A92: ( Int ( @ A1)) meets ( Int ( @ A2));

        consider S1 be c=-linear finite simplex-like Subset-Family of Kas such that

         A93: A1 = (B .: S1) by A2, A90, SIMPLEX0:def 20;

        consider S2 be c=-linear finite simplex-like Subset-Family of Kas such that

         A94: A2 = (B .: S2) by A2, A91, SIMPLEX0:def 20;

        ( card ( union S1)) <= ( card ( union S2)) or ( card ( union S2)) <= ( card ( union S1));

        hence A1 = A2 by A89, A90, A91, A92, A93, A94;

      end;

      hence thesis by Th25;

    end;

    registration

      let V, K;

      cluster ( BCS K) -> simplex-join-closed;

      coherence

      proof

        ( [#] K) = the carrier of V by SIMPLEX0:def 10;

        then |.K.| c= ( [#] K);

        hence thesis by Th29;

      end;

      let n;

      cluster ( BCS (n,K)) -> simplex-join-closed;

      coherence

      proof

        defpred P[ Nat] means ( BCS ($1,K)) is simplex-join-closed affinely-independent;

        ( [#] K) = ( [#] V) by SIMPLEX0:def 10;

        then

         A1: |.K.| c= ( [#] K);

        

         A2: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A3: P[n];

          ( BCS ((n + 1),K)) = ( BCS ( BCS (n,K))) by A1, Th20;

          hence thesis by A3;

        end;

        

         A4: P[ 0 qua Nat] by A1, Th16;

        for n holds P[n] from NAT_1:sch 2( A4, A2);

        hence thesis;

      end;

    end

    theorem :: SIMPLEX1:30

    

     Th30: |.Kv.| c= ( [#] Kv) & (for n st n <= ( degree Kv) holds ex S be Simplex of Kv st ( card S) = (n + 1) & ( @ S) is affinely-independent) implies ( degree Kv) = ( degree ( BCS Kv))

    proof

      assume that

       A1: |.Kv.| c= ( [#] Kv) and

       A2: for n st n <= ( degree Kv) holds ex S be Simplex of Kv st ( card S) = (n + 1) & ( @ S) is affinely-independent;

      

       A3: ( dom ( center_of_mass V)) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

      

       A4: for n st n <= ( degree Kv) holds ex S be Subset of Kv st S is simplex-like & ( card S) = (n + 1) & ( BOOL S) c= ( dom ( center_of_mass V)) & (( center_of_mass V) .: ( BOOL S)) is Subset of Kv & (( center_of_mass V) | ( BOOL S)) is one-to-one

      proof

        let n;

        assume n <= ( degree Kv);

        then

        consider S be Simplex of Kv such that

         A5: ( card S) = (n + 1) and

         A6: ( @ S) is affinely-independent by A2;

        take S;

        thus S is simplex-like & ( card S) = (n + 1) by A5;

        

         A7: the topology of ( Complex_of {( @ S)}) = ( bool S) by SIMPLEX0: 4;

        reconsider SS = {( @ S)} as affinely-independent Subset-Family of V by A6;

        

         A8: (( center_of_mass V) .: ( BOOL S)) c= ( conv ( @ S))

        proof

          let y be object;

          assume y in (( center_of_mass V) .: ( BOOL S));

          then

          consider x be object such that

           A9: x in ( dom ( center_of_mass V)) and

           A10: x in ( BOOL S) & (( center_of_mass V) . x) = y by FUNCT_1:def 6;

          reconsider x as non empty Subset of V by A9, ZFMISC_1: 56;

          ( conv x) c= ( conv ( @ S)) & y in ( conv x) by A10, RLAFFIN2: 16, RLTOPSP1: 20;

          hence thesis;

        end;

        ( bool ( @ S)) c= ( bool the carrier of V) by ZFMISC_1: 67;

        hence ( BOOL S) c= ( dom ( center_of_mass V)) by A3, XBOOLE_1: 33;

        ( conv ( @ S)) c= |.Kv.| by Th5;

        then ( conv ( @ S)) c= ( [#] Kv) by A1;

        hence (( center_of_mass V) .: ( BOOL S)) is Subset of Kv by A8, XBOOLE_1: 1;

        ((( center_of_mass V) | ( bool S)) | ( BOOL S)) = (( center_of_mass V) | ( BOOL S)) & ( Complex_of SS) is SimplicialComplex of V by RELAT_1: 74;

        hence thesis by A6, A7, FUNCT_1: 52;

      end;

       not {} in ( dom ( center_of_mass V)) by ZFMISC_1: 56;

      then

       A11: ( dom ( center_of_mass V)) is with_non-empty_elements;

      ( BCS Kv) = ( subdivision (( center_of_mass V),Kv)) by A1, Def5;

      hence thesis by A4, A11, SIMPLEX0: 53;

    end;

    theorem :: SIMPLEX1:31

    

     Th31: |.Ka.| c= ( [#] Ka) implies ( degree Ka) = ( degree ( BCS Ka))

    proof

      

       A1: for n st n <= ( degree Ka) holds ex S be Simplex of Ka st ( card S) = (n + 1) & ( @ S) is affinely-independent

      proof

        let n;

        reconsider N = n as ExtReal;

        set S = the Simplex of n, Ka;

        assume n <= ( degree Ka);

        then

         A2: ( card S) = (N + 1) by SIMPLEX0:def 18;

        (N + 1) = (n + 1) & ( @ S) is affinely-independent by XXREAL_3:def 2;

        hence thesis by A2;

      end;

      assume |.Ka.| c= ( [#] Ka);

      hence thesis by A1, Th30;

    end;

    theorem :: SIMPLEX1:32

    

     Th32: |.Ka.| c= ( [#] Ka) implies ( degree Ka) = ( degree ( BCS (n,Ka)))

    proof

      defpred P[ Nat] means ( degree Ka) = ( degree ( BCS ($1,Ka))) & ( BCS ($1,Ka)) is non void affinely-independent;

      assume

       A1: |.Ka.| c= ( [#] Ka);

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A3: P[n];

        

         A4: ( [#] ( BCS (n,Ka))) = ( [#] Ka) by A1, Th18;

        ( BCS ((n + 1),Ka)) = ( BCS ( BCS (n,Ka))) & |.( BCS (n,Ka)).| = |.Ka.| by A1, Th10, Th20;

        hence thesis by A1, A3, A4, Th28, Th31;

      end;

      

       A5: P[ 0 qua Nat] by A1, Th16;

      for n holds P[n] from NAT_1:sch 2( A5, A2);

      hence thesis;

    end;

    theorem :: SIMPLEX1:33

    

     Th33: for S be simplex-like Subset-Family of Kas st S is with_non-empty_elements holds ( card S) = ( card (( center_of_mass V) .: S))

    proof

      set B = ( center_of_mass V);

      set T = the topology of Kas;

      let S be simplex-like Subset-Family of Kas such that

       A1: S is with_non-empty_elements;

      

       A2: not {} in S by A1;

      ( [#] Kas) c= the carrier of V by SIMPLEX0:def 9;

      then ( bool the carrier of Kas) c= ( bool the carrier of V) by ZFMISC_1: 67;

      then ( dom B) = (( bool the carrier of V) \ { {} }) & S c= ( bool the carrier of V) by FUNCT_2:def 1;

      then

       A3: ( dom (B | S)) = S by A2, RELAT_1: 62, ZFMISC_1: 34;

      S c= T

      proof

        let x be object;

        assume x in S;

        then x is Simplex of Kas by TOPS_2:def 1;

        hence thesis by PRE_TOPC:def 2;

      end;

      then ((B | T) | S) = (B | S) by RELAT_1: 74;

      then

       A4: (B | S) is one-to-one by FUNCT_1: 52;

      (B .: S) = ( rng (B | S)) by RELAT_1: 115;

      then (S,(B .: S)) are_equipotent by A3, A4, WELLORD2:def 4;

      hence thesis by CARD_1: 5;

    end;

    reserve Aff for finite affinely-independent Subset of V,

Af,Bf for finite Subset of V,

B for Subset of V,

S,T for finite Subset-Family of V,

Sf for c=-linear finite finite-membered Subset-Family of V,

Sk,Tk for finite simplex-like Subset-Family of K,

Ak for Simplex of K;

    theorem :: SIMPLEX1:34

    

     Th34: for S1,S2 be simplex-like Subset-Family of Kas st |.Kas.| c= ( [#] Kas) & S1 is with_non-empty_elements & (( center_of_mass V) .: S2) is Simplex of ( BCS Kas) & (( center_of_mass V) .: S1) c= (( center_of_mass V) .: S2) holds S1 c= S2 & S2 is c=-linear

    proof

      set B = ( center_of_mass V);

      set BK = ( BCS Kas);

      let S1,S2 be simplex-like Subset-Family of Kas;

      assume that

       A1: |.Kas.| c= ( [#] Kas) and

       A2: S1 is with_non-empty_elements and

       A3: (B .: S2) is Simplex of ( BCS Kas) and

       A4: (B .: S1) c= (B .: S2);

      BK = ( subdivision (B,Kas)) by A1, Def5;

      then

      consider W2 be c=-linear finite simplex-like Subset-Family of Kas such that

       A5: (B .: S2) = (B .: W2) by A3, SIMPLEX0:def 20;

      reconsider s2 = (S2 \ { {} }) as simplex-like Subset-Family of Kas by TOPS_2: 11, XBOOLE_1: 36;

      set TK = the topology of Kas;

      set BTK = (B | TK);

      

       A6: ( dom BTK) = (( dom B) /\ TK) by RELAT_1: 61;

      

       A7: s2 c= TK by SIMPLEX0: 14;

      

       A8: ( dom B) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

      then (( @ S2) \ { {} }) c= ( dom B) by XBOOLE_1: 33;

      then s2 c= (( dom B) /\ TK) by A7, XBOOLE_1: 19;

      then

       A9: s2 c= ( dom BTK) by RELAT_1: 61;

      (W2 /\ ( dom B)) c= W2 by XBOOLE_1: 17;

      then

      reconsider w2 = (W2 /\ ( dom B)) as c=-linear finite simplex-like Subset-Family of Kas by TOPS_2: 11, XBOOLE_1: 1;

      

       A10: w2 c= TK by SIMPLEX0: 14;

      then

       A11: (B .: W2) = (B .: (W2 /\ ( dom B))) & (B .: w2) = (BTK .: w2) by RELAT_1: 112, RELAT_1: 129;

      (W2 /\ ( dom B)) c= ( dom B) by XBOOLE_1: 17;

      then

       A12: w2 c= ( dom BTK) by A6, A10, XBOOLE_1: 19;

      S2 c= TK by SIMPLEX0: 14;

      then (B .: S2) = (BTK .: S2) by RELAT_1: 129;

      then

       A13: w2 c= S2 by A5, A11, A12, FUNCT_1: 87;

      

       A14: S1 c= TK by SIMPLEX0: 14;

      (S2 /\ ( dom B)) = ((( @ S2) /\ ( bool the carrier of V)) \ { {} }) by A8, XBOOLE_1: 49

      .= s2 by XBOOLE_1: 28;

      then

       A15: (B .: S2) = (B .: s2) by RELAT_1: 112;

      then (BTK .: s2) = (B .: S2) by A7, RELAT_1: 129;

      then

       A16: s2 c= w2 by A5, A11, A9, FUNCT_1: 87;

      ( @ S1) c= ( bool the carrier of V) & not {} in S1 by A2;

      then S1 c= ( dom B) by A8, ZFMISC_1: 34;

      then

       A17: S1 c= ( dom BTK) by A6, A14, XBOOLE_1: 19;

      (B .: S1) = (BTK .: S1) by A14, RELAT_1: 129;

      then S1 c= w2 by A4, A5, A11, A17, FUNCT_1: 87;

      hence S1 c= S2 by A13;

      let x, y such that

       A18: x in S2 & y in S2;

      (B .: s2) = (BTK .: s2) by A7, RELAT_1: 129;

      then w2 c= s2 by A5, A11, A12, A15, FUNCT_1: 87;

      then

       A19: s2 = w2 by A16;

      per cases ;

        suppose x is empty or y is empty;

        then x c= y or y c= x;

        hence thesis;

      end;

        suppose x is non empty & y is non empty;

        then x in w2 & y in w2 by A18, A19, ZFMISC_1: 56;

        hence thesis by ORDINAL1:def 8;

      end;

    end;

    theorem :: SIMPLEX1:35

    

     Th35: S is with_non-empty_elements & ( union S) c= Aff & ((( card S) + n) + 1) <= ( card Aff) implies (Bf is Simplex of (n + ( card S)), ( BCS ( Complex_of {Aff})) & (( center_of_mass V) .: S) c= Bf iff ex T st T misses S & (T \/ S) is c=-linear with_non-empty_elements & ( card T) = (n + 1) & ( union T) c= Aff & Bf = ((( center_of_mass V) .: S) \/ (( center_of_mass V) .: T)))

    proof

      set B = ( center_of_mass V), U = ( union S);

      assume that

       A1: S is with_non-empty_elements and

       A2: U c= Aff and

       A3: ((( card S) + n) + 1) <= ( card Aff);

      set C = ( Complex_of {Aff});

      reconsider c = ( card Aff) as ExtReal;

      set BTC = (B | the topology of C);

      set BC = ( BCS C);

      

       A4: the topology of C = ( bool Aff) by SIMPLEX0: 4;

      

       A5: ( degree C) = (c - 1) by SIMPLEX0: 26

      .= (( card Aff) + ( - 1)) by XXREAL_3:def 2;

      reconsider c = (( card S) + n) as ExtReal;

      

       A6: |.C.| c= ( [#] C);

      then

       A7: BC = ( subdivision (B,C)) by Def5;

      (( card S) + n) <= (( card Aff) - 1) by A3, XREAL_1: 19;

      then

       A8: (( card S) + n) <= ( degree BC) by A5, A6, Th31;

      hereby

        

         A9: S c= the topology of C

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in S;

          then xx c= U by ZFMISC_1: 74;

          then xx c= Aff by A2;

          hence thesis by A4;

        end;

        then

         A10: (B .: S) = (BTC .: S) by RELAT_1: 129;

        ( dom B) = (( bool the carrier of V) \ { {} }) & not {} in S by A1, FUNCT_2:def 1;

        then ( dom BTC) = (( dom B) /\ the topology of C) & S c= ( dom B) by RELAT_1: 61, ZFMISC_1: 34;

        then

         A11: S c= ( dom BTC) by A9, XBOOLE_1: 19;

        assume that

         A12: Bf is Simplex of (n + ( card S)), ( BCS ( Complex_of {Aff})) and

         A13: (B .: S) c= Bf;

        consider a be c=-linear finite simplex-like Subset-Family of C such that

         A14: Bf = (B .: a) by A7, A12, SIMPLEX0:def 20;

        (a /\ ( dom B)) c= a by XBOOLE_1: 17;

        then

        reconsider AA = (a /\ ( dom B)) as c=-linear finite simplex-like Subset-Family of C by TOPS_2: 11, XBOOLE_1: 1;

        

         A15: (B .: S) c= (B .: AA) by A13, A14, RELAT_1: 112;

        reconsider T = (AA \ S) as Subset-Family of V;

        

         A16: AA c= the topology of C by SIMPLEX0: 14;

        then

         A17: (B .: AA) = (BTC .: AA) by RELAT_1: 129;

        

         A18: (S \/ T) = (AA \/ S) by XBOOLE_1: 39

        .= AA by A10, A11, A15, A17, FUNCT_1: 87, XBOOLE_1: 12;

        T c= AA by XBOOLE_1: 36;

        then

         A19: T c= ( bool Aff) by A4, A16;

        

         A20: not {} in AA by ZFMISC_1: 56;

        then (B .: a) = (B .: (a /\ ( dom B))) & AA is with_non-empty_elements by RELAT_1: 112;

        then

         A21: ( card Bf) = ( card AA) by A14, Th33;

        

         A22: Bf = (B .: AA) by A14, RELAT_1: 112

        .= ((B .: S) \/ (B .: T)) by A18, RELAT_1: 120;

        reconsider T as finite Subset-Family of V;

        take T;

        ( card Bf) = (c + 1) by A8, A12, SIMPLEX0:def 18

        .= ((( card S) + n) + 1) by XXREAL_3:def 2;

        then ( union ( bool Aff)) = Aff & (( card S) + ( card (AA \ S))) = ((( card S) + n) + 1) by A18, A21, CARD_2: 40, XBOOLE_1: 79, ZFMISC_1: 81;

        hence T misses S & (T \/ S) is c=-linear with_non-empty_elements & ( card T) = (n + 1) & ( union T) c= Aff & Bf = ((B .: S) \/ (B .: T)) by A18, A19, A20, A22, XBOOLE_1: 79, ZFMISC_1: 77;

      end;

      given T be finite Subset-Family of V such that

       A23: T misses S and

       A24: (T \/ S) is c=-linear with_non-empty_elements and

       A25: ( card T) = (n + 1) and

       A26: ( union T) c= Aff and

       A27: Bf = ((( center_of_mass V) .: S) \/ (( center_of_mass V) .: T));

      reconsider TS = (T \/ S) as Subset-Family of C;

      reconsider t = T as finite Subset-Family of V;

      

       A28: ( card TS) = (( card t) + ( card S)) by A23, CARD_2: 40

      .= ((( card S) + n) + 1) by A25;

      ( union (T \/ S)) = (( union T) \/ ( union S)) by ZFMISC_1: 78;

      then ( union (T \/ S)) c= Aff by A2, A26, XBOOLE_1: 8;

      then (T \/ S) c= ( bool ( union (T \/ S))) & ( bool ( union (T \/ S))) c= ( bool Aff) by ZFMISC_1: 67, ZFMISC_1: 82;

      then

       A29: (T \/ S) c= the topology of C by A4;

      

       A30: TS is simplex-like

      proof

        let a be Subset of C;

        thus thesis by A29;

      end;

      ( [#] BC) = ( [#] C) by A7, SIMPLEX0:def 20;

      then

      reconsider BTS = (B .: TS) as Simplex of BC by A7, A24, A30, SIMPLEX0:def 20;

      ( card TS) = ( card (B .: TS)) by A24, A30, Th33;

      then

       A31: ( card BTS) = (c + 1) by A28, XXREAL_3:def 2;

      BTS = Bf by A27, RELAT_1: 120;

      hence thesis by A8, A27, A31, SIMPLEX0:def 18, XBOOLE_1: 7;

    end;

    theorem :: SIMPLEX1:36

    

     Th36: Sf is with_non-empty_elements & ( union Sf) c= Aff implies ((( center_of_mass V) .: Sf) is Simplex of (( card ( union Sf)) - 1), ( BCS ( Complex_of {Aff})) iff for n st 0 < n & n <= ( card ( union Sf)) holds ex x st x in Sf & ( card x) = n)

    proof

      reconsider N = 0 as Nat;

      set U = ( union Sf);

      assume that

       A1: Sf is with_non-empty_elements and

       A2: ( union Sf) c= Aff;

      set B = ( center_of_mass V), C = ( Complex_of {Aff});

      reconsider s = Sf as c=-linear finite Subset-Family of C;

      

       A3: the topology of C = ( bool Aff) by SIMPLEX0: 4;

      ( Segm ( card U)) c= ( Segm ( card Aff)) by A2, CARD_1: 11;

      then ( card U) <= ( card Aff) by NAT_1: 39;

      then

       A4: (N - 1) <= (( card U) - 1) & (( card U) - 1) <= (( card Aff) - 1) by XREAL_1: 9;

      Sf c= ( bool U) & ( bool U) c= ( bool Aff) by A2, ZFMISC_1: 67, ZFMISC_1: 82;

      then

       A5: s c= the topology of C by A3;

      

       A6: s is simplex-like

      proof

        let a be Subset of C;

        assume a in s;

        hence thesis by A5;

      end;

      then

       A7: ( card s) = ( card (B .: Sf)) by A1, Th33;

      ( Segm ( card Sf)) c= ( Segm ( card U)) by A1, SIMPLEX0: 10;

      then

       A8: ( card Sf) <= ( card U) by NAT_1: 39;

      set BC = ( BCS C);

      reconsider c = ( card Aff) as ExtReal;

      

       A9: ( degree C) = (c - 1) by SIMPLEX0: 26

      .= (( card Aff) + ( - 1)) by XXREAL_3:def 2;

      

       A10: |.C.| c= ( [#] C);

      then

       A11: BC = ( subdivision (B,C)) by Def5;

      then ( [#] BC) = ( [#] C) by SIMPLEX0:def 20;

      then

      reconsider BS = (B .: Sf) as Subset of BC;

      

       A12: (N - 1) <= (( card Aff) - 1) by XREAL_1: 9;

      

       A13: ( degree BC) = ( degree C) by A10, Th31;

      thus (( center_of_mass V) .: Sf) is Simplex of (( card U) - 1), ( BCS ( Complex_of {Aff})) implies for n st 0 < n & n <= ( card U) holds ex x st x in Sf & ( card x) = n

      proof

        assume (B .: Sf) is Simplex of (( card U) - 1), BC;

        then

        reconsider BS = (B .: Sf) as Simplex of (( card U) - 1), BC;

        reconsider c1 = (( card U) - 1) as ExtReal;

        let n;

        reconsider s = Sf as Subset-Family of U by ZFMISC_1: 82;

        defpred P[ Nat] means $1 < ( card Sf) implies ex x be finite set st x in Sf & ( card x) = (( card Sf) - $1);

        assume that

         A14: 0 < n and

         A15: n <= ( card U);

        

         A16: (( card Sf) - 0 qua Real) > (( card Sf) qua Real - n qua Real) by A14, XREAL_1: 10;

        

         A17: ( card BS) = (c1 + 1) by A4, A9, A13, SIMPLEX0:def 18

        .= ((( card U) - 1) + 1) by XXREAL_3:def 2

        .= ( card U);

        then

         A18: Sf is non empty by A14, A15;

        then

        consider s1 be Subset-Family of U such that

         A19: s c= s1 and s1 is with_non-empty_elements c=-linear and

         A20: ( card U) = ( card s1) and

         A21: for Z be set st Z in s1 & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in s1 by A1, SIMPLEX0: 9, SIMPLEX0: 13;

        ( card U) = ( card Sf) by A1, A6, A17, Th33;

        then

         A22: s = s1 by A19, A20, CARD_2: 102;

        

         A23: for n st P[n] holds P[(n + 1)]

        proof

          let n such that

           A24: P[n];

          assume

           A25: (n + 1) < ( card Sf);

          then

          consider X be finite set such that

           A26: X in Sf and

           A27: ( card X) = (( card Sf) - n) by A24, NAT_1: 13;

          

           A28: ((n + 1) - n) < (( card Sf) - n) by A25, XREAL_1: 9;

          then

          consider x such that

           A29: x in X & (X \ {x}) in Sf by A21, A22, A26, A27;

          reconsider C = (( card X) - 1) as Element of NAT by A27, A28, NAT_1: 20;

          take (X \ {x});

          ( card X) = (C + 1);

          hence thesis by A27, A29, STIRL2_1: 55;

        end;

        

         A30: P[ 0 qua Nat] by A7, A17, A18, SIMPLEX0: 9;

        

         A31: for n holds P[n] from NAT_1:sch 2( A30, A23);

        (( card Sf) - n) is Nat by A7, A15, A17, NAT_1: 21;

        then ex x be finite set st x in Sf & ( card x) = (( card Sf) - (( card Sf) - n)) by A16, A31;

        hence thesis;

      end;

      assume

       A32: for n st 0 < n & n <= ( card U) holds ex x st x in Sf & ( card x) = n;

      per cases ;

        suppose

         A33: U is empty;

        reconsider O = ( - 1) as ExtReal;

        

         A34: O <= ( degree BC) & 0 = (O + 1) by A9, A10, A12, Th31, XXREAL_3: 7;

        Sf is empty by A1, A33;

        then

         A35: BS is empty;

        thus thesis by A33, A34, A35, SIMPLEX0:def 18;

      end;

        suppose

         A36: U is non empty;

        reconsider c1 = (( card U) - 1) as ExtReal;

        consider x such that

         A37: x in Sf and ( card x) = ( card U) by A32, A36;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & ( card D2) = $1;

        

         A38: for x be object st x in ( Seg ( card U)) holds ex y be object st y in Sf & P[x, y]

        proof

          let x be object such that

           A39: x in ( Seg ( card U));

          reconsider n = x as Nat by A39;

           0 < n & n <= ( card U) by A39, FINSEQ_1: 1;

          then ex x st x in Sf & ( card x) = n by A32;

          hence thesis;

        end;

        consider f be Function of ( Seg ( card U)), Sf such that

         A40: for x be object st x in ( Seg ( card U)) holds P[x, (f . x)] from FUNCT_2:sch 1( A38);

        now

          let x1,x2 be object;

          assume that

           A41: x1 in ( dom f) and

           A42: x2 in ( dom f) & (f . x1) = (f . x2);

          

           A43: P[x2, (f . x2)] by A40, A42;

           P[x1, (f . x1)] by A40, A41;

          

          hence x1 = ( card (f . x1))

          .= x2 by A42, A43;

        end;

        then

         A44: ( rng f) c= Sf & f is one-to-one by FUNCT_1:def 4;

        ( dom f) = ( Seg ( card U)) by A37, FUNCT_2:def 1;

        then ( Segm ( card ( Seg ( card U)))) = ( Segm ( card U)) & ( Segm ( card ( Seg ( card U)))) c= ( Segm ( card Sf)) by A44, CARD_1: 10, FINSEQ_1: 57;

        then ( card U) <= ( card Sf) by NAT_1: 39;

        then

         A45: ( card BS) = ( card U) by A7, A8, XXREAL_0: 1;

        BS is Simplex of BC & (c1 + 1) = ((( card U) - 1) + 1) by A6, A11, SIMPLEX0:def 20, XXREAL_3:def 2;

        hence thesis by A4, A9, A13, A45, SIMPLEX0:def 18;

      end;

    end;

    

     Lm1: for S be finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & ( card S) = ( card ( union S)) holds for A be non empty finite Subset of V st A misses ( union S) & (( union S) \/ A) is affinely-independent holds ((( center_of_mass V) .: S) \/ (( center_of_mass V) .: {(( union S) \/ A)})) is Simplex of ( card S), ( BCS ( Complex_of {(( union S) \/ A)}))

    proof

      let S be finite finite-membered Subset-Family of V such that

       A1: S is c=-linear and

       A2: S is with_non-empty_elements and

       A3: ( card S) = ( card ( union S));

      set U = ( union S), B = ( center_of_mass V);

      let A be non empty finite Subset of V such that

       A4: A misses U and

       A5: (U \/ A) is affinely-independent;

      reconsider UA = (U \/ A) as finite affinely-independent Subset of V by A5;

      set C = ( Complex_of {UA});

      reconsider SUA = (S \/ {UA}) as Subset-Family of C;

      

       A6: U c= UA by XBOOLE_1: 7;

      

       A7: the topology of C = ( bool UA) by SIMPLEX0: 4;

      

       A8: SUA c= the topology of C

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in SUA;

        then x in S or x in {UA} by XBOOLE_0:def 3;

        then xx c= U or x = UA by TARSKI:def 1, ZFMISC_1: 74;

        then xx c= UA by A6;

        hence thesis by A7;

      end;

      

       A9: SUA is simplex-like

      proof

        let A be Subset of C;

        assume A in SUA;

        hence thesis by A8;

      end;

      set BC = ( BCS C);

      

       A10: |.C.| c= ( [#] C);

      then

       A11: BC = ( subdivision (B,C)) by Def5;

      then ( [#] BC) = ( [#] C) by SIMPLEX0:def 20;

      then

      reconsider BSUA = (B .: SUA) as Subset of BC;

      SUA is c=-linear

      proof

        let x,y be set such that

         A12: x in SUA & y in SUA;

        per cases by A12, XBOOLE_0:def 3;

          suppose x in S & y in S;

          hence thesis by A1;

        end;

          suppose x in S & y in {UA};

          then x c= U & y = UA by TARSKI:def 1, ZFMISC_1: 74;

          then x c= y by A6;

          hence thesis;

        end;

          suppose x in {UA} & y in S;

          then x = UA & y c= U by TARSKI:def 1, ZFMISC_1: 74;

          then y c= x by A6;

          hence thesis;

        end;

          suppose

           A13: x in {UA} & y in {UA};

          then x = UA by TARSKI:def 1;

          hence thesis by A13, TARSKI:def 1;

        end;

      end;

      then

      reconsider BSUA as Simplex of BC by A9, A11, SIMPLEX0:def 20;

      reconsider c = ( card UA) as ExtReal;

      

       A14: ( degree C) = (c - 1) by SIMPLEX0: 26

      .= (( card UA) + ( - 1)) by XXREAL_3:def 2;

      

       A15: UA <> U

      proof

        assume UA = U;

        then A c= U by XBOOLE_1: 7;

        hence contradiction by A4, XBOOLE_1: 67;

      end;

       not UA in S by ZFMISC_1: 74, A6, A15;

      then

       A16: ( card SUA) = (( card S) + 1) by CARD_2: 41;

      U c< UA by A6, A15;

      then ( card U) < ( card UA) by CARD_2: 48;

      then (( card U) + 1) <= ( card UA) by NAT_1: 13;

      then

       A17: ( card U) <= (( card UA) - 1) by XREAL_1: 19;

      reconsider c = ( card S) as ExtReal;

      ( card BSUA) = ( card SUA) by A2, A9, Th33;

      then

       A18: ( card BSUA) = (c + 1) by A16, XXREAL_3:def 2;

      ( degree BC) = ( degree C) by A10, Th31;

      then BSUA is Simplex of ( card S), BC by A3, A14, A17, A18, SIMPLEX0:def 18;

      hence thesis by RELAT_1: 120;

    end;

    theorem :: SIMPLEX1:37

    

     Th37: for S st S is c=-linear & S is with_non-empty_elements & ( card S) = ( card ( union S)) holds for Af, Bf st Af is non empty & Af misses ( union S) & (( union S) \/ Af) is affinely-independent & (( union S) \/ Af) c= Bf holds ((( center_of_mass V) .: S) \/ (( center_of_mass V) .: {(( union S) \/ Af)})) is Simplex of ( card S), ( BCS ( Complex_of {Bf}))

    proof

      let S be finite Subset-Family of V such that

       A1: S is c=-linear & S is with_non-empty_elements and

       A2: ( card S) = ( card ( union S));

      set U = ( union S), b = ( center_of_mass V);

      let A,B be finite Subset of V such that

       A3: A is non empty and

       A4: A misses U & (U \/ A) is affinely-independent and

       A5: (U \/ A) c= B;

      reconsider UA = (U \/ A) as finite Subset of V by A5;

      ( dom b) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

      then UA in ( dom b) by A3, ZFMISC_1: 56;

      

      then

       A6: {(b . UA)} = ( Im (b,UA)) by FUNCT_1: 59

      .= (b .: {UA}) by RELAT_1:def 16;

      set CA = ( Complex_of {UA});

      set CB = ( Complex_of {B});

       {UA} is_finer_than {B}

      proof

        let x;

        assume x in {UA};

        then

         A7: x = UA by TARSKI:def 1;

        B in {B} by TARSKI:def 1;

        hence thesis by A5, A7;

      end;

      then CA is SubSimplicialComplex of CB by SIMPLEX0: 30;

      then

       A8: ( subdivision (b,CA)) is SubSimplicialComplex of ( subdivision (b,CB)) by SIMPLEX0: 58;

       |.CA.| c= ( [#] CA);

      then

       A9: ( subdivision (b,CA)) = ( BCS CA) by Def5;

       |.CB.| c= ( [#] CB);

      then

       A10: ( BCS CA) is SubSimplicialComplex of ( BCS CB) by A8, A9, Def5;

      S is finite-membered

      proof

        let x;

        assume x in S;

        then

         A11: x c= ( union S) by ZFMISC_1: 74;

        ( union S) is finite by A2;

        hence thesis by A11;

      end;

      then ((b .: S) \/ (b .: {UA})) is Simplex of ( card S), ( BCS CA) by A1, A2, A3, A4, Lm1;

      hence thesis by A6, A10, SIMPLEX0: 49;

    end;

    theorem :: SIMPLEX1:38

    

     Th38: for Sf st Sf is with_non-empty_elements & ( card Sf) = ( card ( union Sf)) holds for v be Element of V st not v in ( union Sf) & (( union Sf) \/ {v}) is affinely-independent holds { S1 where S1 be Simplex of ( card Sf), ( BCS ( Complex_of {(( union Sf) \/ {v})})) : (( center_of_mass V) .: Sf) c= S1 } = {((( center_of_mass V) .: Sf) \/ (( center_of_mass V) .: {(( union Sf) \/ {v})}))}

    proof

      let S be finite c=-linear finite-membered Subset-Family of V such that

       A1: S is with_non-empty_elements and

       A2: ( card S) = ( card ( union S));

      set U = ( union S);

      set B = ( center_of_mass V);

      let v be Element of V such that

       A3: not v in U and

       A4: (U \/ {v}) is affinely-independent;

      reconsider Uv = (U \/ {v}) as finite affinely-independent Subset of V by A4;

      set CUv = ( Complex_of {Uv});

      set BC = ( BCS CUv);

      set SS = { S1 where S1 be Simplex of ( card S), ( BCS ( Complex_of {(( union S) \/ {v})})) : (B .: S) c= S1 };

      set TT = {((B .: S) \/ (B .: {(( union S) \/ {v})}))};

      

       A5: U c= Uv by XBOOLE_1: 7;

      hereby

        let x be object;

        reconsider n = 0 as Nat;

        assume x in SS;

        then

        consider S1 be Simplex of ( card S), BC such that

         A6: x = S1 and

         A7: (B .: S) c= S1;

        ((( card S) + n) + 1) <= ( card Uv) by A2, A3, CARD_2: 41;

        then

        consider T be finite Subset-Family of V such that

         A8: T misses S and

         A9: (T \/ S) is c=-linear with_non-empty_elements and

         A10: ( card T) = (n + 1) and

         A11: ( union T) c= Uv and

         A12: ( @ S1) = ((( center_of_mass V) .: S) \/ (( center_of_mass V) .: T)) by A1, A5, A7, Th35;

        

         A13: ex x be object st T = {x} by A10, CARD_2: 42;

        

         A14: ( union (T \/ S)) = (( union T) \/ ( union S)) by ZFMISC_1: 78;

        (T \/ S) is finite-membered

        proof

          let x;

          assume x in (T \/ S);

          then x c= ( union (T \/ S)) by ZFMISC_1: 74;

          hence thesis by A11, A14;

        end;

        then

        reconsider TS = (T \/ S) as finite finite-membered Subset-Family of V;

        ( union (T \/ S)) c= Uv by A5, A11, A14, XBOOLE_1: 8;

        then

         A15: ( card ( union TS)) c= ( card Uv) by CARD_1: 11;

        ( card TS) = (( card S) + 1) by A8, A10, CARD_2: 40;

        then

         A16: ( card TS) = ( card Uv) by A2, A3, CARD_2: 41;

        ( card TS) c= ( card ( union TS)) by A9, SIMPLEX0: 10;

        then ( card ( union TS)) = ( card TS) by A15, A16;

        then

         A17: ( union TS) = Uv by A5, A11, A14, A16, CARD_2: 102, XBOOLE_1: 8;

        

         A18: ( union S) c= ( union (T \/ S)) by A14, XBOOLE_1: 7;

        

         A19: not ( union TS) in S

        proof

          assume ( union TS) in S;

          then ( union TS) c= U by ZFMISC_1: 74;

          then

           A20: U = Uv by A17, A18;

          v in {v} by TARSKI:def 1;

          hence thesis by A3, A20, XBOOLE_0:def 3;

        end;

        T is non empty by A10;

        then ( union TS) in TS by A9, SIMPLEX0: 9;

        then ( union TS) in T by A19, XBOOLE_0:def 3;

        then T = {Uv} by A13, A17, TARSKI:def 1;

        hence x in TT by A6, A12, TARSKI:def 1;

      end;

      let x be object;

      assume x in TT;

      then

       A21: x = ((B .: S) \/ (B .: {Uv})) by TARSKI:def 1;

      (B .: S) c= ((B .: S) \/ (B .: {Uv})) & ((B .: S) \/ (B .: {Uv})) is Simplex of ( card S), BC by A1, A2, A3, Th37, XBOOLE_1: 7, ZFMISC_1: 50;

      hence thesis by A21;

    end;

    theorem :: SIMPLEX1:39

    

     Th39: for Sf st Sf is with_non-empty_elements & (( card Sf) + 1) = ( card ( union Sf)) & ( union Sf) is affinely-independent holds ( card { S1 where S1 be Simplex of ( card Sf), ( BCS ( Complex_of {( union Sf)})) : (( center_of_mass V) .: Sf) c= S1 }) = 2

    proof

      let S be finite c=-linear finite-membered Subset-Family of V such that

       A1: S is with_non-empty_elements and

       A2: (( card S) + 1) = ( card ( union S)) and

       A3: ( union S) is affinely-independent;

      set B = ( center_of_mass V);

      reconsider U = ( union S) as finite affinely-independent Subset of V by A3;

      reconsider s = S as Subset-Family of U by ZFMISC_1: 82;

      

       A4: S is non empty by A2, ZFMISC_1: 2;

      then

      consider ss1 be Subset-Family of U such that

       A5: s c= ss1 and

       A6: ss1 is with_non-empty_elements c=-linear and

       A7: ( card ss1) = ( card U) and

       A8: for X st X in ss1 & ( card X) <> 1 holds ex x st x in X & (X \ {x}) in ss1 by A1, SIMPLEX0: 9, SIMPLEX0: 13;

      ( card (ss1 \ s)) = ((( card S) + 1) - ( card S)) by A2, A5, A7, CARD_2: 44;

      then

      consider x be object such that

       A9: (ss1 \ s) = {x} by CARD_2: 42;

      reconsider c = ( card U) as ExtReal;

      set CU = ( Complex_of {U});

      set TC = the topology of CU;

      

       A10: TC = ( bool U) by SIMPLEX0: 4;

      then

      reconsider ss = ss1 as Subset-Family of CU by XBOOLE_1: 1;

      set BC = ( BCS CU);

      reconsider cc = (( card U) - 1) as ExtReal;

      

       A11: |.CU.| c= ( [#] CU);

      then

       A12: BC = ( subdivision (B,CU)) by Def5;

      then

       A13: ( [#] BC) = ( [#] CU) by SIMPLEX0:def 20;

      then

      reconsider Bss = (B .: ss) as Subset of BC;

      

       A14: ss is simplex-like

      proof

        let A be Subset of CU;

        assume A in ss;

        hence thesis by A10;

      end;

      then

       A15: ( card Bss) = ( card U) by A6, A7, Th33;

      then

       A16: ( card Bss) = (cc + 1) by A2, XXREAL_3:def 2;

      

       A17: x in {x} by TARSKI:def 1;

      then

       A18: x in ss1 by A9, XBOOLE_0:def 5;

      

       A19: not x in s by A9, A17, XBOOLE_0:def 5;

      reconsider x as finite Subset of V by A9, A17, XBOOLE_1: 1;

      ( degree CU) = (c - 1) by SIMPLEX0: 26

      .= (( card U) + ( - 1)) by XXREAL_3:def 2;

      then

       A20: cc = ( degree BC) by A11, Th31;

      Bss is simplex-like by A6, A12, A14, SIMPLEX0:def 20;

      then

       A21: Bss is Simplex of (( card U) - 1), BC by A2, A16, A20, SIMPLEX0:def 18;

      x <> {} by A6, A18;

      then

      reconsider c1 = (( card x) - 1) as Element of NAT by NAT_1: 20;

      ex xm be set st (xm in s or xm = {} ) & ( card xm) = (( card x) - 1) & for y st y in s & y c= x holds y c= xm

      proof

        per cases ;

          suppose

           A22: ( card x) = 1;

          then

           A23: ex z be object st x = {z} by CARD_2: 42;

          take xm = {} ;

          thus (xm in s or xm = {} ) & ( card xm) = (( card x) - 1) by A22;

          let y such that

           A24: y in s and

           A25: y c= x;

          y <> x by A9, A17, A24, XBOOLE_0:def 5;

          hence thesis by A23, A25, ZFMISC_1: 33;

        end;

          suppose ( card x) <> 1;

          then

          consider z be set such that

           A26: z in x and

           A27: (x \ {z}) in ss1 by A8, A18;

          take xm = (x \ {z});

          

           A28: x = (xm \/ {z}) by A26, ZFMISC_1: 116;

          xm in s

          proof

            assume not xm in s;

            then xm in (ss1 \ s) by A27, XBOOLE_0:def 5;

            then xm = x by A9, TARSKI:def 1;

            hence thesis by A26, ZFMISC_1: 56;

          end;

          hence xm in s or xm = {} ;

          ( card x) = (c1 + 1);

          hence ( card xm) = (( card x) - 1) by A26, STIRL2_1: 55;

          let y such that

           A29: y in s and

           A30: y c= x;

          assume

           A31: not y c= xm;

          (xm,y) are_c=-comparable by A5, A6, A27, A29;

          then xm c= y by A31;

          hence contradiction by A19, A28, A29, A30, A31, ZFMISC_1: 138;

        end;

      end;

      then

      consider xm be set such that

       A32: xm in s or xm = {} and

       A33: ( card xm) = (( card x) - 1) and

       A34: for y st y in s & y c= x holds y c= xm;

      

       A35: U in S by A4, SIMPLEX0: 9;

      then ( union ss1) c= U & U c= ( union ss) by A5, ZFMISC_1: 74;

      then

       A36: ( union ss) = U;

      x c< U by A9, A17, A19, A35;

      then ( card x) < ( card U) by CARD_2: 48;

      then (( card x) + 1) <= ( card U) by NAT_1: 13;

      then

      consider xM be set such that

       A37: xM in ss and

       A38: ( card xM) = (( card x) + 1) by A6, A36, A21, Th36;

      reconsider xm as finite Subset of V by A32, XBOOLE_1: 2;

      reconsider xM as finite Subset of V by A37;

      

       A39: not xM c= xm

      proof

        assume xM c= xm;

        then (( card x) + 1) <= (( card x) + ( - 1)) by A33, A38, NAT_1: 43;

        hence contradiction by XREAL_1: 6;

      end;

      

       A40: xM in s

      proof

        assume not xM in s;

        then xM in (ss \ s) by A37, XBOOLE_0:def 5;

        then xM = x by A9, TARSKI:def 1;

        hence contradiction by A38;

      end;

      then (xm,xM) are_c=-comparable or xm c= xM by A32, ORDINAL1:def 8;

      then

       A41: xm c= xM by A39;

      then ( card (xM \ xm)) = (( card xM) - ( card xm)) by CARD_2: 44;

      then

      consider x1,x2 be object such that

       A42: x1 <> x2 and

       A43: (xM \ xm) = {x1, x2} by A33, A38, CARD_2: 60;

      

       A44: x1 in {x1, x2} by TARSKI:def 2;

      

       A45: x2 in {x1, x2} by TARSKI:def 2;

      then

      reconsider x1, x2 as Element of V by A43, A44;

      set xm1 = (xm \/ {x1}), xm2 = (xm \/ {x2});

      reconsider S1 = (S \/ {xm1}), S2 = (S \/ {xm2}) as Subset-Family of CU;

      reconsider BS1 = (B .: S1), BS2 = (B .: S2) as Subset of BC by A13;

      

       A46: BS1 = ((B .: S) \/ (B .: {xm1})) by RELAT_1: 120;

      

       A47: not x1 in xm by A43, A44, XBOOLE_0:def 5;

      then

       A48: ( card xm1) = (( card xm) + 1) by CARD_2: 41;

      

       A49: not xm1 in S

      proof

        assume

         A50: xm1 in S;

        then (x,xm1) are_c=-comparable by A5, A6, A18;

        then x c= xm1 or xm1 c= x;

        hence thesis by A19, A33, A48, A50, CARD_2: 102;

      end;

       not x2 in xm by A43, A45, XBOOLE_0:def 5;

      then

       A51: ( card xm2) = (( card xm) + 1) by CARD_2: 41;

      

       A52: not xm2 in S

      proof

        assume

         A53: xm2 in S;

        then (x,xm2) are_c=-comparable by A5, A6, A18;

        then x c= xm2 or xm2 c= x;

        hence thesis by A19, A33, A51, A53, CARD_2: 102;

      end;

      x2 in xM by A43, A45, XBOOLE_0:def 5;

      then {x2} c= xM by ZFMISC_1: 31;

      then

       A54: xm2 c= xM by A41, XBOOLE_1: 8;

      

       A55: S2 c= ( bool U)

      proof

        let A be object such that

         A56: A in S2;

        reconsider AA = A as set by TARSKI: 1;

        per cases by A56, XBOOLE_0:def 3;

          suppose A in S;

          then AA c= U by ZFMISC_1: 74;

          hence thesis;

        end;

          suppose A in {xm2};

          then A = xm2 by TARSKI:def 1;

          then AA c= U by A37, A54, XBOOLE_1: 1;

          hence thesis;

        end;

      end;

      

       A57: S2 is simplex-like

      proof

        let A be Subset of CU;

        assume A in S2;

        hence thesis by A10, A55;

      end;

      then ( card BS2) = ( card S2) by A1, Th33;

      then

       A58: ( card BS2) = (( card S) + 1) by A52, CARD_2: 41;

      x1 in xM by A43, A44, XBOOLE_0:def 5;

      then {x1} c= xM by ZFMISC_1: 31;

      then

       A59: xm1 c= xM by A41, XBOOLE_1: 8;

      

       A60: S1 c= ( bool U)

      proof

        let A be object such that

         A61: A in S1;

        reconsider AA = A as set by TARSKI: 1;

        per cases by A61, XBOOLE_0:def 3;

          suppose A in S;

          then AA c= U by ZFMISC_1: 74;

          hence thesis;

        end;

          suppose A in {xm1};

          then A = xm1 by TARSKI:def 1;

          then AA c= U by A37, A59, XBOOLE_1: 1;

          hence thesis;

        end;

      end;

      then

       A62: BS1 = ((B | TC) .: S1) by A10, RELAT_1: 129;

      

       A63: S1 is simplex-like

      proof

        let A be Subset of CU;

        assume A in S1;

        hence thesis by A10, A60;

      end;

      then ( card BS1) = ( card S1) by A1, Th33;

      then

       A64: ( card BS1) = (( card S) + 1) by A49, CARD_2: 41;

      

       A65: xm c= xm1 & xm c= xm2 by XBOOLE_1: 7;

      

       A66: for y1 be set st y1 in S holds (y1,xm1) are_c=-comparable & (y1,xm2) are_c=-comparable

      proof

        let y1 be set;

        assume

         A67: y1 in S;

        then

         A68: (xM,y1) are_c=-comparable by A40, ORDINAL1:def 8;

        per cases by A68;

          suppose xM c= y1 or xM = y1;

          then xm1 c= y1 & xm2 c= y1 by A54, A59;

          hence thesis;

        end;

          suppose

           A69: y1 c= xM & xM <> y1;

          then

          reconsider y1 as finite set;

          

           A70: y1 c< xM by A69;

          

           A71: not x c= y1

          proof

            

             A72: ( card y1) < ( card xM) by A70, CARD_2: 48;

            assume

             A73: x c= y1;

            then ( card x) <= ( card y1) by NAT_1: 43;

            then ( card x) = ( card y1) by A38, A72, NAT_1: 9;

            hence contradiction by A19, A67, A73, CARD_2: 102;

          end;

          x in ss by A9, A17, XBOOLE_0:def 5;

          then (y1,x) are_c=-comparable by A5, A6, A67;

          then y1 c= x by A71;

          then y1 c= xm by A34, A67;

          then y1 c= xm1 & y1 c= xm2 by A65;

          hence thesis;

        end;

      end;

      S1 is c=-linear

      proof

        let y1,y2 be set;

        assume that

         A74: y1 in S1 and

         A75: y2 in S1;

        y1 in S or y1 in {xm1} by A74, XBOOLE_0:def 3;

        then

         A76: y1 in S or y1 = xm1 by TARSKI:def 1;

        y2 in S or y2 in {xm1} by A75, XBOOLE_0:def 3;

        then y2 in S or y2 = xm1 by TARSKI:def 1;

        hence thesis by A66, A76, ORDINAL1:def 8;

      end;

      then BS1 is simplex-like by A12, A63, SIMPLEX0:def 20;

      then

       A77: BS1 is Simplex of (( card U) - 1), BC by A2, A15, A16, A20, A64, SIMPLEX0:def 18;

      set SS = { S3 where S3 be Simplex of ( card S), ( BCS ( Complex_of {( union S)})) : (B .: S) c= S3 };

      (B .: S) c= ((B .: S) \/ (B .: {xm1})) by XBOOLE_1: 7;

      then

       A78: BS1 in SS by A2, A46, A77;

      

       A79: BS2 = ((B .: S) \/ (B .: {xm2})) by RELAT_1: 120;

      

       A80: SS c= {BS1, BS2}

      proof

        let w be object;

        reconsider n = 0 as Nat;

        assume w in SS;

        then

        consider W be Simplex of ( card S), BC such that

         A81: w = W and

         A82: (B .: S) c= W;

        ((( card S) + n) + 1) <= ( card U) by A2;

        then

        consider T be finite Subset-Family of V such that

         A83: T misses S and

         A84: (T \/ S) is c=-linear with_non-empty_elements and

         A85: ( card T) = (n + 1) and

         A86: ( union T) c= U and

         A87: ( @ W) = ((B .: S) \/ (B .: T)) by A1, A82, Th35;

        consider x3 be object such that

         A88: {x3} = T by A85, CARD_2: 42;

        

         A89: x3 in T by A88, TARSKI:def 1;

        then

         A90: not x3 in S by A83, XBOOLE_0: 3;

        reconsider x3 as set by TARSKI: 1;

        

         A91: x3 c= ( union T) by A89, ZFMISC_1: 74;

        

         A92: x3 in (T \/ S) by A89, XBOOLE_0:def 3;

        reconsider x3 as finite Subset of U by A86, A91, XBOOLE_1: 1;

        

         A93: not xM c= x3

        proof

          consider x4 be set such that

           A94: x4 in ss and

           A95: ( card x4) = ( card x3) by A6, A36, A21, A84, A92, Th36, NAT_1: 43;

          assume xM c= x3;

          then (( card x) + 1) <= ( card x3) by A38, NAT_1: 43;

          then x <> x4 by A95, NAT_1: 13;

          then not x4 in {x} by TARSKI:def 1;

          then

           A96: x4 in s by A9, A94, XBOOLE_0:def 5;

          then x4 in (S \/ T) by XBOOLE_0:def 3;

          then (x3,x4) are_c=-comparable by A84, A92;

          then x3 c= x4 or x4 c= x3;

          hence contradiction by A90, A95, A96, CARD_2: 102;

        end;

        

         A97: xm c= x3 & xm <> x3

        proof

          per cases by A32;

            suppose xm = {} ;

            hence thesis by A84, A92;

          end;

            suppose

             A98: xm in s;

            

             A99: not x3 c= xm

            proof

              assume x3 c= xm;

              then

               A100: ( card x3) <= ( card xm) by NAT_1: 43;

              consider x4 be set such that

               A101: x4 in ss and

               A102: ( card x4) = ( card x3) by A6, A36, A21, A84, A92, Th36, NAT_1: 43;

              (( card xm) + 1) = ( card x) by A33;

              then ( card x) <> ( card x3) by A100, NAT_1: 13;

              then not x4 in {x} by A102, TARSKI:def 1;

              then

               A103: x4 in s by A9, A101, XBOOLE_0:def 5;

              then x4 in (S \/ T) by XBOOLE_0:def 3;

              then (x3,x4) are_c=-comparable by A84, A92;

              then x3 c= x4 or x4 c= x3;

              hence contradiction by A90, A102, A103, CARD_2: 102;

            end;

            xm in (T \/ S) by A98, XBOOLE_0:def 3;

            then (xm,x3) are_c=-comparable by A84, A92;

            hence thesis by A99;

          end;

        end;

        then

         A104: x3 = (x3 \/ xm) by XBOOLE_1: 12;

        xM in (S \/ T) by A40, XBOOLE_0:def 3;

        then (xM,x3) are_c=-comparable by A84, A92;

        then x3 c= xM by A93;

        then

         A105: (x3 \ xm) c= (xM \ xm) by XBOOLE_1: 33;

        

         A106: xM = (xm \/ xM) by A41, XBOOLE_1: 12;

        

         A107: (x3 \ xm) <> (xM \ xm)

        proof

          assume (x3 \ xm) = (xM \ xm);

          then x3 = ((xM \ xm) \/ xm) by A104, XBOOLE_1: 39;

          hence contradiction by A93, A106, XBOOLE_1: 39;

        end;

        

         A108: (x3 \ xm) <> {} by XBOOLE_1: 37, A97;

        (x3 \/ xm) = ((x3 \ xm) \/ xm) by XBOOLE_1: 39;

        then x3 = xm1 or x3 = xm2 by A43, A104, A105, A107, A108, ZFMISC_1: 36;

        hence thesis by A79, A46, A81, A87, A88, TARSKI:def 2;

      end;

      

       A109: BS2 = ((B | TC) .: S2) by A10, A55, RELAT_1: 129;

      

       A110: BS1 <> BS2

      proof

        assume

         A111: BS1 = BS2;

        then (BS1 \ BS2) = {} by XBOOLE_1: 37;

        then ((B | TC) .: (S1 \ S2)) = {} by A109, A62, FUNCT_1: 64;

        then

         A112: ( dom (B | TC)) misses (S1 \ S2) by RELAT_1: 118;

        (BS2 \ BS1) = {} by A111, XBOOLE_1: 37;

        then ((B | TC) .: (S2 \ S1)) = {} by A109, A62, FUNCT_1: 64;

        then

         A113: ( dom (B | TC)) misses (S2 \ S1) by RELAT_1: 118;

        

         A114: ( dom (B | TC)) = (( dom B) /\ TC) by RELAT_1: 61;

        xm1 in {xm1} by TARSKI:def 1;

        then

         A115: xm1 in S1 by XBOOLE_0:def 3;

        

         A116: ( dom B) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

        

         A117: (S1 \ S2) c= S1 by XBOOLE_1: 36;

        then not {} in (S1 \ S2) by A1;

        then

         A118: (S1 \ S2) c= ( dom B) by A116, ZFMISC_1: 34;

        

         A119: (S2 \ S1) c= S2 by XBOOLE_1: 36;

        then not {} in (S2 \ S1) by A1;

        then

         A120: (S2 \ S1) c= ( dom B) by A116, ZFMISC_1: 34;

        (S1 \ S2) c= ( bool U) by A60, A117;

        then (S1 \ S2) c= ( dom (B | TC)) by A10, A114, A118, XBOOLE_1: 19;

        then

         A121: (S1 \ S2) = {} by A112, XBOOLE_1: 67;

        (S2 \ S1) c= ( bool U) by A55, A119;

        then (S2 \ S1) c= ( dom (B | TC)) by A10, A114, A120, XBOOLE_1: 19;

        then S1 = S2 by A113, A121, XBOOLE_1: 32, XBOOLE_1: 67;

        then xm1 in {xm2} by A49, A115, XBOOLE_0:def 3;

        then

         A122: xm1 = xm2 by TARSKI:def 1;

        x1 in {x1} by TARSKI:def 1;

        then x1 in xm1 by XBOOLE_0:def 3;

        then x1 in {x2} by A47, A122, XBOOLE_0:def 3;

        hence contradiction by A42, TARSKI:def 1;

      end;

      S2 is c=-linear

      proof

        let y1,y2 be set;

        assume that

         A123: y1 in S2 and

         A124: y2 in S2;

        y1 in S or y1 in {xm2} by A123, XBOOLE_0:def 3;

        then

         A125: y1 in S or y1 = xm2 by TARSKI:def 1;

        y2 in S or y2 in {xm2} by A124, XBOOLE_0:def 3;

        then y2 in S or y2 = xm2 by TARSKI:def 1;

        hence thesis by A66, A125, ORDINAL1:def 8;

      end;

      then BS2 is simplex-like by A12, A57, SIMPLEX0:def 20;

      then

       A126: BS2 is Simplex of (( card U) - 1), BC by A2, A15, A16, A20, A58, SIMPLEX0:def 18;

      (B .: S) c= ((B .: S) \/ (B .: {xm2})) by XBOOLE_1: 7;

      then BS2 in SS by A2, A79, A126;

      then {BS1, BS2} c= SS by A78, ZFMISC_1: 32;

      then SS = {BS1, BS2} by A80;

      hence thesis by A110, CARD_2: 57;

    end;

    theorem :: SIMPLEX1:40

    

     Th40: Aff is Simplex of K implies (B is Simplex of ( BCS ( Complex_of {Aff})) iff B is Simplex of ( BCS K) & ( conv B) c= ( conv Aff))

    proof

      set Bag = ( center_of_mass V);

      set C = ( Complex_of {Aff});

      

       A1: the topology of C = ( bool Aff) by SIMPLEX0: 4;

      assume Aff is Simplex of K;

      then

      reconsider s = Aff as Simplex of K;

      

       A2: ( [#] K) = the carrier of V by SIMPLEX0:def 10;

      then |.K.| c= ( [#] K);

      then

       A3: ( subdivision (Bag,K)) = ( BCS K) by Def5;

      ( @ s) is affinely-independent;

      then

       A4: ( Complex_of {Aff}) is SubSimplicialComplex of K by Th3;

      then the topology of C c= the topology of K by SIMPLEX0:def 13;

      then

       A5: |.C.| c= |.K.| by Th4;

      ( [#] C) = ( [#] V);

      then

       A6: ( subdivision (Bag,C)) = ( BCS C) by A5, Def5;

      then ( BCS C) is SubSimplicialComplex of ( BCS K) by A3, A4, SIMPLEX0: 58;

      then

       A7: the topology of ( BCS C) c= the topology of ( BCS K) by SIMPLEX0:def 13;

      hereby

        assume B is Simplex of ( BCS C);

        then

        reconsider A = B as Simplex of ( BCS C);

        A in the topology of ( BCS C) by PRE_TOPC:def 2;

        then A in the topology of ( BCS K) by A7;

        then

        reconsider a = A as Simplex of ( BCS K) by PRE_TOPC:def 2;

         |.( BCS C).| = |.C.| & ( conv ( @ A)) c= |.( BCS C).| by Th5, Th10;

        then ( conv ( @ a)) c= ( conv Aff) by Th8;

        hence B is Simplex of ( BCS K) & ( conv B) c= ( conv Aff);

      end;

      assume that

       A8: B is Simplex of ( BCS K) and

       A9: ( conv B) c= ( conv Aff);

      reconsider A = B as Simplex of ( BCS K) by A8;

      consider SS be c=-linear finite simplex-like Subset-Family of K such that

       A10: B = (Bag .: SS) by A3, A8, SIMPLEX0:def 20;

      reconsider ss = SS as c=-linear finite Subset-Family of C by A2;

      ( [#] ( subdivision (Bag,C))) = ( [#] C) by SIMPLEX0:def 20;

      then

      reconsider Bss = (Bag .: ss) as Subset of ( BCS C) by A5, Def5;

      

       A11: ( dom Bag) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

      ss is simplex-like

      proof

        let a be Subset of C such that

         A12: a in ss;

        reconsider aK = a as Simplex of K by A12, TOPS_2:def 1;

        per cases ;

          suppose aK is empty;

          hence thesis;

        end;

          suppose

           A13: aK is non empty;

          then aK in ( dom Bag) by A11, ZFMISC_1: 56;

          then

           A14: (Bag . aK) in A by A10, A12, FUNCT_1:def 6;

          

           A15: (Bag . aK) in ( Int ( @ aK)) by A13, RLAFFIN2: 20;

          A c= ( conv ( @ A)) by RLAFFIN1: 2;

          then (Bag . aK) in ( conv ( @ A)) by A14;

          then ( Int ( @ aK)) meets ( conv ( @ s)) by A9, A15, XBOOLE_0: 3;

          then aK c= Aff by Th26;

          hence thesis by A1;

        end;

      end;

      then Bss is simplex-like by A6, SIMPLEX0:def 20;

      hence thesis by A10;

    end;

    theorem :: SIMPLEX1:41

    

     Th41: Sk is with_non-empty_elements & (( card Sk) + n) <= ( degree K) implies (Af is Simplex of (n + ( card Sk)), ( BCS K) & (( center_of_mass V) .: Sk) c= Af iff ex Tk st Tk misses Sk & (Tk \/ Sk) is c=-linear with_non-empty_elements & ( card Tk) = (n + 1) & Af = ((( center_of_mass V) .: Sk) \/ (( center_of_mass V) .: Tk)))

    proof

      set B = ( center_of_mass V);

      set BK = ( BCS K);

      assume that

       A1: Sk is with_non-empty_elements and

       A2: (( card Sk) + n) <= ( degree K);

      reconsider nc = (n + ( card Sk)) as ExtReal;

      

       A3: ((nc + 1) - 1) = nc by XXREAL_3: 22;

      

       A4: ( [#] K) = the carrier of V by SIMPLEX0:def 10;

      then

       A5: |.K.| c= ( [#] K);

      then

       A6: ( subdivision (B,K)) = BK by Def5;

      

       A7: nc <= ( degree BK) by A2, A5, Th31;

      hereby

        assume that

         A8: Af is Simplex of (n + ( card Sk)), BK and

         A9: (B .: Sk) c= Af;

        consider T be c=-linear finite simplex-like Subset-Family of K such that

         A10: Af = (B .: T) by A6, A8, SIMPLEX0:def 20;

        ( union T) is empty or ( union T) in T by SIMPLEX0: 9, ZFMISC_1: 2;

        then

         A11: ( union T) is simplex-like by TOPS_2:def 1;

        then ( @ ( union T)) is affinely-independent;

        then

        reconsider UT = ( union T) as finite affinely-independent Subset of V;

        UT = ( union ( @ T));

        then ( conv Af) c= ( conv UT) by A10, CONVEX1: 30, RLAFFIN2: 17;

        then

        reconsider s1 = Af as Simplex of ( BCS ( Complex_of {UT})) by A8, A11, Th40;

        ( card Af) = (nc + 1) by A7, A8, SIMPLEX0:def 18;

        then

         A12: s1 is Simplex of (n + ( card Sk)), ( BCS ( Complex_of {UT})) by A3, SIMPLEX0: 48;

        set C = ( Complex_of {UT});

        reconsider cT = ( card UT) as ExtReal;

         |.C.| c= ( [#] C);

        then

         A13: ( degree C) = ( degree ( BCS C)) by Th31;

        ( degree C) = (cT - 1) & ( card s1) <= (( degree ( BCS C)) + 1) by SIMPLEX0: 24, SIMPLEX0: 26;

        then ( card s1) <= ( card UT) by A13, XXREAL_3: 22;

        then (nc + 1) <= ( card UT) by A7, A8, SIMPLEX0:def 18;

        then

         A14: ((( card Sk) + n) + 1) <= ( card UT) by XXREAL_3:def 2;

        ( the_family_of K) is subset-closed & UT in the topology of K by A11;

        then

         A15: ( bool UT) c= the topology of K by SIMPLEX0: 1;

        ( union ( @ Sk)) c= ( union T) by A1, A5, A8, A9, A10, Th34, ZFMISC_1: 77;

        then

        consider R be finite Subset-Family of V such that

         A16: R misses Sk & (R \/ Sk) is c=-linear with_non-empty_elements & ( card R) = (n + 1) and

         A17: ( union R) c= UT and

         A18: Af = ((( center_of_mass V) .: Sk) \/ (( center_of_mass V) .: R)) by A1, A9, A12, A14, Th35;

        reconsider R as Subset-Family of K by A4;

        R c= ( bool ( union R)) & ( bool ( union R)) c= ( bool UT) by A17, SIMPLEX0: 1, ZFMISC_1: 82;

        then R c= ( bool UT);

        then R c= the topology of K by A15;

        then

        reconsider R as simplex-like finite Subset-Family of K by SIMPLEX0: 14;

        take R;

        thus R misses Sk & (R \/ Sk) is c=-linear with_non-empty_elements & ( card R) = (n + 1) & Af = ((B .: Sk) \/ (B .: R)) by A16, A18;

      end;

      given T be simplex-like finite Subset-Family of K such that

       A19: T misses Sk and

       A20: (T \/ Sk) is c=-linear with_non-empty_elements and

       A21: ( card T) = (n + 1) and

       A22: Af = ((B .: Sk) \/ (B .: T));

      set ST = (Sk \/ T);

      ( [#] K) = ( [#] BK) by A6, SIMPLEX0:def 20;

      then

      reconsider BST = (B .: ST) as Subset of BK by SIMPLEX0:def 10;

      

       A23: ST is simplex-like by TOPS_2: 13;

      then

      reconsider BST as Simplex of BK by A6, A20, SIMPLEX0:def 20;

      ( card ST) = (( card Sk) + ( card T)) by A19, CARD_2: 40;

      then ( card BST) = ((( card Sk) + n) + 1) by A20, A21, A23, Th33;

      then ((B .: Sk) \/ (B .: T)) = (B .: ST) & ( card BST) = (nc + 1) by RELAT_1: 120, XXREAL_3:def 2;

      hence thesis by A3, A22, SIMPLEX0: 48, XBOOLE_1: 7;

    end;

    theorem :: SIMPLEX1:42

    

     Th42: Sk is c=-linear with_non-empty_elements & ( card Sk) = ( card ( union Sk)) & ( union Sk) c= Ak & ( card Ak) = (( card Sk) + 1) implies { S1 where S1 be Simplex of ( card Sk), ( BCS K) : (( center_of_mass V) .: Sk) c= S1 & ( conv ( @ S1)) c= ( conv ( @ Ak)) } = {((( center_of_mass V) .: Sk) \/ (( center_of_mass V) .: {Ak}))}

    proof

      set B = ( center_of_mass V);

      assume that

       A1: Sk is c=-linear with_non-empty_elements and

       A2: ( card Sk) = ( card ( union Sk)) and

       A3: ( union Sk) c= Ak and

       A4: ( card Ak) = (( card Sk) + 1);

      ( card (Ak \ ( union Sk))) = ((( card Sk) + 1) - ( card Sk)) by A2, A3, A4, CARD_2: 44

      .= 1;

      then

      consider v be object such that

       A5: (Ak \ ( union Sk)) = {v} by CARD_2: 42;

      reconsider Ak1 = ( @ Ak) as affinely-independent finite Subset of V;

      set C = ( Complex_of {Ak1});

      reconsider c = ( card Ak) as ExtReal;

      

       A6: ( degree C) = (c - 1) by SIMPLEX0: 26

      .= (( card Ak) + ( - 1)) by XXREAL_3:def 2

      .= ( card Sk) by A4;

      reconsider Sk1 = ( @ Sk) as c=-linear finite finite-membered Subset-Family of V by A1;

      set XX = { W where W be Simplex of ( card Sk), ( BCS C) : (B .: Sk) c= W };

      set YY = { W where W be Simplex of ( card Sk), ( BCS K) : (B .: Sk) c= W & ( conv ( @ W)) c= ( conv ( @ Ak)) };

      ( [#] K) = the carrier of V by SIMPLEX0:def 10;

      then |.K.| c= ( [#] K);

      then

       A7: ( subdivision (B,K)) = ( BCS K) by Def5;

      

       A8: C is SubSimplicialComplex of K by Th3;

      then the topology of C c= the topology of K by SIMPLEX0:def 13;

      then

       A9: |.C.| c= |.K.| by Th4;

      

       A10: ( [#] C) = ( [#] V);

      then

       A11: ( degree C) = ( degree ( BCS C)) by A9, Th31;

      ( subdivision (B,C)) = ( BCS C) by A9, A10, Def5;

      then ( BCS C) is SubSimplicialComplex of ( BCS K) by A7, A8, SIMPLEX0: 58;

      then

       A12: ( degree ( BCS C)) <= ( degree ( BCS K)) by SIMPLEX0: 32;

      

       A13: XX c= YY

      proof

        let x be object;

        assume x in XX;

        then

        consider W be Simplex of ( card Sk), ( BCS C) such that

         A14: x = W & (B .: Sk1) c= W;

        W = ( @ W);

        then

        reconsider w = W as Simplex of ( BCS K) by Th40;

        ( card W) = (( degree ( BCS C)) + 1) by A6, A11, SIMPLEX0:def 18;

        then

         A15: w is Simplex of ( card Sk), ( BCS K) by A6, A11, A12, SIMPLEX0:def 18;

        ( conv ( @ W)) c= ( conv ( @ Ak)) & ( @ w) = w by Th40;

        hence thesis by A14, A15;

      end;

      

       A16: ( [#] ( subdivision (B,C))) = ( [#] C) by SIMPLEX0:def 20;

      

       A17: YY c= XX

      proof

        let x be object;

        reconsider c1 = ( card Sk) as ExtReal;

        assume x in YY;

        then

        consider W be Simplex of ( card Sk), ( BCS K) such that

         A18: W = x & (B .: Sk) c= W and

         A19: ( conv ( @ W)) c= ( conv ( @ Ak));

        reconsider w = ( @ W) as Subset of ( BCS C) by A9, A16, Def5;

        reconsider cW = ( card W) as ExtReal;

        ( card W) = (c1 + 1) by A6, A11, A12, SIMPLEX0:def 18

        .= (( card Sk) + 1) by XXREAL_3:def 2;

        then ( card Sk) = (( card W) + ( - 1));

        then

         A20: ( card Sk) = (cW - 1) by XXREAL_3:def 2;

        w is simplex-like by A19, Th40;

        then w is Simplex of ( card Sk), ( BCS C) by A20, SIMPLEX0: 48;

        hence thesis by A18;

      end;

      v in {v} by TARSKI:def 1;

      then

       A21: v in Ak1 & not v in ( union Sk) by A5, XBOOLE_0:def 5;

      Ak = (Ak \/ ( union Sk)) by A3, XBOOLE_1: 12

      .= ( {v} \/ ( union Sk1)) by A5, XBOOLE_1: 39;

      then XX = {((B .: Sk1) \/ (B .: {Ak}))} by A1, A2, A21, Th38;

      hence thesis by A13, A17;

    end;

    theorem :: SIMPLEX1:43

    

     Th43: Sk is c=-linear with_non-empty_elements & (( card Sk) + 1) = ( card ( union Sk)) implies ( card { S1 where S1 be Simplex of ( card Sk), ( BCS K) : (( center_of_mass V) .: Sk) c= S1 & ( conv ( @ S1)) c= ( conv ( @ ( union Sk))) }) = 2

    proof

      set B = ( center_of_mass V);

      assume that

       A1: Sk is c=-linear with_non-empty_elements and

       A2: (( card Sk) + 1) = ( card ( union Sk));

      Sk is non empty by A2, ZFMISC_1: 2;

      then ( union Sk) in Sk by A1, SIMPLEX0: 9;

      then

      reconsider U = ( union Sk) as Simplex of K by TOPS_2:def 1;

      reconsider Sk1 = ( @ Sk) as c=-linear finite finite-membered Subset-Family of V by A1;

      reconsider c = ( card U) as ExtReal;

      ( @ U) = ( union Sk1);

      then

      reconsider U1 = ( union Sk1) as finite affinely-independent Subset of V;

      set C = ( Complex_of {U1});

      

       A3: ( degree C) = (c - 1) by SIMPLEX0: 26

      .= (( card U) + ( - 1)) by XXREAL_3:def 2

      .= ( card Sk) by A2;

      set YY = { W where W be Simplex of ( card Sk), ( BCS K) : (B .: Sk) c= W & ( conv ( @ W)) c= ( conv ( @ ( union Sk))) };

      ( [#] K) = the carrier of V by SIMPLEX0:def 10;

      then |.K.| c= ( [#] K);

      then

       A4: ( subdivision (B,K)) = ( BCS K) by Def5;

      set XX = { W where W be Simplex of ( card Sk), ( BCS C) : (B .: Sk) c= W };

      

       A5: ( @ U) = U1;

      then

       A6: C is SubSimplicialComplex of K by Th3;

      then the topology of C c= the topology of K by SIMPLEX0:def 13;

      then

       A7: |.C.| c= |.K.| by Th4;

      

       A8: ( [#] C) = ( [#] V);

      then

       A9: ( degree C) = ( degree ( BCS C)) by A7, Th31;

      ( subdivision (B,C)) = ( BCS C) by A7, A8, Def5;

      then ( BCS C) is SubSimplicialComplex of ( BCS K) by A4, A6, SIMPLEX0: 58;

      then

       A10: ( degree ( BCS C)) <= ( degree ( BCS K)) by SIMPLEX0: 32;

      

       A11: XX c= YY

      proof

        let x be object;

        assume x in XX;

        then

        consider W be Simplex of ( card Sk), ( BCS C) such that

         A12: x = W & (B .: Sk1) c= W;

        W = ( @ W);

        then

        reconsider w = W as Simplex of ( BCS K) by A5, Th40;

        ( card W) = (( degree ( BCS C)) + 1) by A3, A9, SIMPLEX0:def 18;

        then

         A13: w is Simplex of ( card Sk), ( BCS K) by A3, A9, A10, SIMPLEX0:def 18;

        ( conv ( @ W)) c= ( conv ( @ U)) & ( @ w) = w by Th40;

        hence thesis by A12, A13;

      end;

      

       A14: ( [#] ( subdivision (B,C))) = ( [#] C) by SIMPLEX0:def 20;

      

       A15: YY c= XX

      proof

        let x be object;

        reconsider c1 = ( card Sk) as ExtReal;

        assume x in YY;

        then

        consider W be Simplex of ( card Sk), ( BCS K) such that

         A16: W = x & (B .: Sk) c= W and

         A17: ( conv ( @ W)) c= ( conv ( @ U));

        reconsider w = ( @ W) as Subset of ( BCS C) by A7, A14, Def5;

        reconsider cW = ( card W) as ExtReal;

        ( card W) = (c1 + 1) by A3, A9, A10, SIMPLEX0:def 18

        .= (( card Sk) + 1) by XXREAL_3:def 2;

        then ( card Sk) = (( card W) + ( - 1));

        then

         A18: ( card Sk) = (cW - 1) by XXREAL_3:def 2;

        w is simplex-like by A17, Th40;

        then w is Simplex of ( card Sk), ( BCS C) by A18, SIMPLEX0: 48;

        hence thesis by A16;

      end;

      ( card XX) = 2 by A1, A2, Th39;

      hence thesis by A11, A15, XBOOLE_0:def 10;

    end;

    theorem :: SIMPLEX1:44

    

     Th44: for Af st K is Subdivision of ( Complex_of {Af}) & ( card Af) = (n + 1) & ( degree K) = n & for S be Simplex of (n - 1), K, X st X = { S1 where S1 be Simplex of n, K : S c= S1 } holds (( conv ( @ S)) meets ( Int Af) implies ( card X) = 2) & (( conv ( @ S)) misses ( Int Af) implies ( card X) = 1) holds for S be Simplex of (n - 1), ( BCS K), X st X = { S1 where S1 be Simplex of n, ( BCS K) : S c= S1 } holds (( conv ( @ S)) meets ( Int Af) implies ( card X) = 2) & (( conv ( @ S)) misses ( Int Af) implies ( card X) = 1)

    proof

      let A be finite Subset of V;

      assume that

       A1: K is Subdivision of ( Complex_of {A}) and

       A2: ( card A) = (n + 1) and

       A3: ( degree K) = n and

       A4: for S be Simplex of (n - 1), K, X be set st X = { S1 where S1 be Simplex of n, K : S c= S1 } holds (( conv ( @ S)) meets ( Int A) implies ( card X) = 2) & (( conv ( @ S)) misses ( Int A) implies ( card X) = 1);

       |.( Complex_of {A}).| = ( conv A) by Th8;

      then

       A5: |.K.| = ( conv A) by A1, Th10;

      

       A6: K is finite-degree by A3, SIMPLEX0:def 12;

      

       A7: A is affinely-independent

      proof

        consider a be Subset of K such that

         A8: a is simplex-like and

         A9: ( card a) = (( degree K) + 1) by A6, SIMPLEX0:def 12;

        ( conv ( @ a)) c= ( conv A) by A5, A8, Th5;

        then

         A10: ( Affin ( @ a)) c= ( Affin A) by RLAFFIN1: 68;

        ( card A) = ( card a) by A2, A3, A9, XXREAL_3:def 2;

        hence thesis by A8, A10, RLAFFIN1: 80;

      end;

      set B = ( center_of_mass V);

      reconsider Z = 0 as Nat;

      set TK = the TopStruct of K;

      reconsider n1 = (n - 1) as ExtReal;

      let S be Simplex of (n - 1), ( BCS K), X be set such that

       A11: X = { S1 where S1 be Simplex of n, ( BCS K) : S c= S1 };

      ( [#] K) = the carrier of V by SIMPLEX0:def 10;

      then

       A12: |.K.| c= ( [#] K);

      then

       A13: ( degree K) = ( degree ( BCS K)) by Th31;

      then

       A14: (n + ( - 1)) >= ( - 1) & (n - 1) <= ( degree ( BCS K)) by A3, XREAL_1: 31, XREAL_1: 146;

      then

       A15: ( card S) = (n1 + 1) by SIMPLEX0:def 18;

      then

       A16: ( card S) = ((n - 1) + 1) by XXREAL_3:def 2;

      

       A17: ( BCS K) = ( subdivision (B,K)) by A12, Def5;

      per cases ;

        suppose

         A18: n = 0 ;

        then

         A19: TK = ( BCS K) by A3, A12, Th21;

        then S in the topology of K by PRE_TOPC:def 2;

        then

        reconsider s = S as Simplex of K by PRE_TOPC:def 2;

        reconsider s as Simplex of (n - 1), K by A3, A15, A18, SIMPLEX0:def 18;

        set XX = { W where W be Simplex of n, K : s c= W };

        

         A20: ( @ S) = ( @ s);

        then

         A21: ( conv ( @ S)) meets ( Int A) implies ( card XX) = 2 by A4;

        

         A22: XX c= X

        proof

          let x be object;

          assume x in XX;

          then

          consider W be Simplex of n, K such that

           A23: x = W & S c= W;

          W in the topology of ( BCS K) by A19, PRE_TOPC:def 2;

          then

          reconsider w = W as Simplex of ( BCS K) by PRE_TOPC:def 2;

          ( card W) = (( degree K) + 1) by A3, SIMPLEX0:def 18;

          then w is Simplex of n, ( BCS K) by A3, A13, SIMPLEX0:def 18;

          hence thesis by A11, A23;

        end;

        

         A24: X c= XX

        proof

          let x be object;

          assume x in X;

          then

          consider W be Simplex of n, ( BCS K) such that

           A25: x = W & S c= W by A11;

          W in the topology of K by A19, PRE_TOPC:def 2;

          then

          reconsider w = W as Simplex of K by PRE_TOPC:def 2;

          ( card W) = (( degree ( BCS K)) + 1) by A3, A13, SIMPLEX0:def 18;

          then w is Simplex of n, K by A3, A13, SIMPLEX0:def 18;

          hence thesis by A25;

        end;

        ( conv ( @ S)) misses ( Int A) implies ( card XX) = 1 by A4, A20;

        hence thesis by A22, A24, A21, XBOOLE_0:def 10;

      end;

        suppose

         A26: n > 0 ;

        consider SS be c=-linear finite simplex-like Subset-Family of K such that

         A27: S = (B .: SS) by A17, SIMPLEX0:def 20;

        (SS \ { {} }) c= SS by XBOOLE_1: 36;

        then

        reconsider SS1 = (SS \ { {} }) as c=-linear finite simplex-like Subset-Family of K by TOPS_2: 11;

        

         A28: SS1 c= ( bool ( @ ( union SS1))) & ( bool ( @ ( union SS1))) c= ( bool the carrier of V) by ZFMISC_1: 67, ZFMISC_1: 82;

        

         A29: not {} in SS1 by ZFMISC_1: 56;

        then

         A30: SS1 is with_non-empty_elements;

        

         A31: ( dom B) = (( bool the carrier of V) \ { {} }) by FUNCT_2:def 1;

        

        then

         A32: (SS /\ ( dom B)) = ((SS /\ ( bool the carrier of V)) \ { {} }) by XBOOLE_1: 49

        .= (SS1 /\ ( bool the carrier of V)) by XBOOLE_1: 49

        .= SS1 by A28, XBOOLE_1: 1, XBOOLE_1: 28;

        then

         A33: (B .: SS) = (B .: SS1) by RELAT_1: 112;

        then

         A34: ( card SS1) = n by A16, A27, A30, Th33;

        

         A35: S = (B .: SS1) by A27, A32, RELAT_1: 112;

        

         A36: ( card SS1) = ( card S) by A27, A30, A33, Th33;

        then

         A37: SS1 is non empty by A16, A26;

        then

         A38: ( union SS1) in SS1 by SIMPLEX0: 9;

        then

        reconsider U = ( union SS1) as Simplex of K by TOPS_2:def 1;

        ( Segm ( card SS1)) c= ( Segm ( card U)) by A30, SIMPLEX0: 10;

        then

         A39: n <= ( card U) by A16, A36, NAT_1: 39;

        ( card U) <= (( degree K) + 1) by SIMPLEX0: 24;

        then

         A40: ( card U) <= (n + 1) by A3, XXREAL_3:def 2;

        

         A41: ( conv ( @ U)) c= ( conv A) by A5, Th5;

        SS1 c= ( bool the carrier of V) by A28;

        then

         A42: ( conv ( @ S)) c= ( conv ( @ U)) by A35, CONVEX1: 30, RLAFFIN2: 17;

        per cases by A39, A40, NAT_1: 9;

          suppose

           A43: ( card U) = n;

          set XX = { W where W be Simplex of n, K : U c= W };

          

           A44: U is Simplex of (n - 1), K by A13, A14, A15, A16, A43, SIMPLEX0:def 18;

          hereby

            assume ( conv ( @ S)) meets ( Int A);

            then ( conv ( @ U)) meets ( Int A) by A42, XBOOLE_1: 63;

            then

             A45: ( card XX) = 2 by A4, A44;

            consider w1,w2 be object such that

             A46: w1 <> w2 and

             A47: XX = {w1, w2} by A45, CARD_2: 60;

            w2 in XX by A47, TARSKI:def 2;

            then

            consider W2 be Simplex of n, K such that

             A48: w2 = W2 and

             A49: U c= W2;

            

             A50: SS1 is with_non-empty_elements & S = (B .: SS1) by A27, A29, A32, RELAT_1: 112;

            w1 in XX by A47, TARSKI:def 2;

            then

            consider W1 be Simplex of n, K such that

             A51: w1 = W1 and

             A52: U c= W1;

            

             A53: ( card W1) = (( degree K) + 1) by A3, SIMPLEX0:def 18;

            then

             A54: ( card W1) = (n + 1) by A3, XXREAL_3:def 2;

            then { W where W be Simplex of n, ( BCS K) : S c= W & ( conv ( @ W)) c= ( conv ( @ W1)) } = {(S \/ (B .: {W1}))} by A16, A27, A30, A33, A36, A43, A52, Th42;

            then (S \/ (B .: {W1})) in { W where W be Simplex of n, ( BCS K) : S c= W & ( conv ( @ W)) c= ( conv ( @ W1)) } by TARSKI:def 1;

            then

             A55: ex R be Simplex of n, ( BCS K) st R = (S \/ (B .: {W1})) & S c= R & ( conv ( @ R)) c= ( conv ( @ W1));

            

             A56: (S \/ (B .: {W1})) <> (S \/ (B .: {W2}))

            proof

              for A be Subset of K st A in {W1} holds A is simplex-like by TARSKI:def 1;

              then {W1} is simplex-like;

              then

               A57: (SS1 \/ {W1}) is simplex-like by TOPS_2: 13;

              

               A58: (S \/ (B .: {W1})) = (B .: (SS1 \/ {W1})) & (S \/ (B .: {W2})) = (B .: (SS1 \/ {W2})) by A35, RELAT_1: 120;

              W1 in {W1} by TARSKI:def 1;

              then

               A59: W1 in (SS1 \/ {W1}) by XBOOLE_0:def 3;

              for A be Subset of K st A in {W2} holds A is simplex-like by TARSKI:def 1;

              then {W2} is simplex-like;

              then

               A60: (SS1 \/ {W2}) is simplex-like by TOPS_2: 13;

              assume

               A61: (S \/ (B .: {W1})) = (S \/ (B .: {W2}));

              W1 is non empty by A3, A53;

              then (SS1 \/ {W1}) c= (SS1 \/ {W2}) by A12, A30, A55, A60, A58, A57, A61, Th34;

              then W1 in SS1 or W1 in {W2} by A59, XBOOLE_0:def 3;

              then W1 c= U by A46, A48, A51, TARSKI:def 1, ZFMISC_1: 74;

              then W1 = U by A52;

              hence contradiction by A43, A54;

            end;

            

             A62: (( card SS1) + Z) <= ( degree K) by A3, A16, A27, A30, A33, Th33;

            

             A63: X c= {(S \/ (B .: {W1})), (S \/ (B .: {W2}))}

            proof

              let x be object;

              

               A64: (n + 1) = (( degree K) + 1) & n = ((( degree K) + 1) - 1) by A3, XXREAL_3: 22, XXREAL_3:def 2;

              assume x in X;

              then

              consider W be Simplex of n, ( BCS K) such that

               A65: x = W and

               A66: S c= W by A11;

              consider T be simplex-like finite Subset-Family of K such that

               A67: T misses SS1 and

               A68: (T \/ SS1) is c=-linear with_non-empty_elements and

               A69: ( card T) = (Z + 1) and

               A70: ( @ W) = ((B .: SS1) \/ (B .: T)) by A16, A36, A50, A62, A66, Th41;

              consider t be object such that

               A71: T = {t} by A69, CARD_2: 42;

              set TS = (T \/ SS1);

              

               A72: ( card TS) = (n + 1) by A16, A36, A67, A69, CARD_2: 40;

              

               A73: ( union TS) in TS by A68, A71, SIMPLEX0: 9;

              TS is simplex-like by TOPS_2: 13;

              then

              reconsider UTS = ( union TS) as Simplex of K by A73;

              ( Segm ( card TS)) c= ( Segm ( card UTS)) by A68, SIMPLEX0: 10;

              then

               A74: ( card TS) <= ( card UTS) by NAT_1: 39;

              UTS in T

              proof

                assume not UTS in T;

                then UTS in SS1 by A73, XBOOLE_0:def 3;

                then ( card UTS) <= ( card U) by NAT_1: 43, ZFMISC_1: 74;

                hence contradiction by A43, A72, A74, NAT_1: 13;

              end;

              then

               A75: UTS = t by A71, TARSKI:def 1;

              ( card UTS) <= (( degree K) + 1) by SIMPLEX0: 24;

              then ( card UTS) <= (n + 1) by A3, XXREAL_3:def 2;

              then ( card UTS) = (n + 1) by A72, A74, XXREAL_0: 1;

              then

               A76: UTS is Simplex of n, K by A64, SIMPLEX0: 48;

              U c= UTS by XBOOLE_1: 7, ZFMISC_1: 77;

              then UTS in XX by A76;

              then W = ((B .: SS1) \/ (B .: {W1})) or W = ((B .: SS1) \/ (B .: {W2})) by A47, A48, A51, A70, A71, A75, TARSKI:def 2;

              hence thesis by A35, A65, TARSKI:def 2;

            end;

            ( card W2) = (( degree K) + 1) by A3, SIMPLEX0:def 18;

            then ( card W2) = (n + 1) by A3, XXREAL_3:def 2;

            then { W where W be Simplex of n, ( BCS K) : S c= W & ( conv ( @ W)) c= ( conv ( @ W2)) } = {(S \/ (B .: {W2}))} by A16, A30, A35, A36, A43, A49, Th42;

            then (S \/ (B .: {W2})) in { W where W be Simplex of n, ( BCS K) : S c= W & ( conv ( @ W)) c= ( conv ( @ W2)) } by TARSKI:def 1;

            then ex R be Simplex of n, ( BCS K) st R = (S \/ (B .: {W2})) & S c= R & ( conv ( @ R)) c= ( conv ( @ W2));

            then

             A77: (S \/ (B .: {W2})) in X by A11;

            (S \/ (B .: {W1})) in X by A11, A55;

            then {(S \/ (B .: {W1})), (S \/ (B .: {W2}))} c= X by A77, ZFMISC_1: 32;

            then X = {(S \/ (B .: {W1})), (S \/ (B .: {W2}))} by A63;

            hence ( card X) = 2 by A56, CARD_2: 57;

          end;

          

           A78: ( conv ( @ S)) c= ( conv A) & A is non empty by A2, A41, A42;

          assume ( conv ( @ S)) misses ( Int A);

          then

          consider BB be Subset of V such that

           A79: BB c< A and

           A80: ( conv ( @ S)) c= ( conv BB) by A7, A78, RLAFFIN2: 23;

          

           A81: BB c= A by A79;

          then

          reconsider B1 = BB as finite Subset of V;

          ( card B1) < (n + 1) by A2, A79, CARD_2: 48;

          then

           A82: ( card B1) <= n by NAT_1: 13;

          ( Affin ( @ S)) c= ( Affin BB) by A80, RLAFFIN1: 68;

          then n <= ( card B1) by A16, RLAFFIN1: 79;

          then ( card B1) = n by A82, XXREAL_0: 1;

          then ( card (A \ BB)) = ((n + 1) - n) by A2, A81, CARD_2: 44;

          then

          consider ab be object such that

           A83: (A \ BB) = {ab} by CARD_2: 42;

          U is non empty by A26, A43;

          then ( @ U) in ( dom B) by A31, ZFMISC_1: 56;

          then

           A84: S c= ( conv ( @ S)) & (B . U) in ( @ S) by A35, A38, FUNCT_1:def 6, RLAFFIN1: 2;

          then (B . U) in ( conv ( @ S));

          then

           A85: (B . U) in ( conv ( @ U)) by A42;

          set BUU = ((B . U) |-- ( @ U));

          ( @ U) c= ( conv ( @ U)) by RLAFFIN1: 2;

          then

           A86: ( @ U) c= ( conv A) by A41;

          

           A87: ab in {ab} by TARSKI:def 1;

          then

          reconsider ab as Element of V by A83;

          

           A88: SS1 is with_non-empty_elements & S = (B .: SS1) by A27, A29, A32, RELAT_1: 112;

          

           A89: ( conv ( @ U)) c= ( Affin ( @ U)) by RLAFFIN1: 65;

          then ( sum BUU) = 1 by A85, RLAFFIN1:def 7;

          then

          consider F be FinSequence of REAL , G be FinSequence of the carrier of V such that

           A90: ((( Sum BUU) |-- A) . ab) = ( Sum F) and

           A91: ( len G) = ( len F) and G is one-to-one and

           A92: ( rng G) = ( Carrier BUU) and

           A93: for n st n in ( dom F) holds (F . n) = ((BUU . (G . n)) * (((G . n) |-- A) . ab)) by A7, A86, RLAFFIN2: 3;

          

           A94: ( dom G) = ( dom F) by A91, FINSEQ_3: 29;

          U c= ( conv B1)

          proof

            

             A95: ( Carrier BUU) c= U by RLVECT_2:def 6;

             A96:

            now

              let i be Nat such that

               A97: i in ( dom F);

              

               A98: (F . i) = ((BUU . (G . i)) * (((G . i) |-- A) . ab)) by A93, A97;

              

               A99: (G . i) in ( rng G) by A94, A97, FUNCT_1:def 3;

              then (G . i) in U by A92, A95;

              then

               A100: (((G . i) |-- A) . ab) >= 0 by A7, A86, RLAFFIN1: 71;

              (BUU . (G . i)) = (1 / ( card U)) by A92, A95, A99, RLAFFIN2: 18;

              hence 0 <= (F . i) by A98, A100;

            end;

            (B . U) in ( conv ( @ S)) by A84;

            then

             A101: (B . U) in ( conv BB) by A80;

            assume not U c= ( conv B1);

            then

            consider t be object such that

             A102: t in U and

             A103: not t in ( conv B1);

            reconsider tt = t as set by TARSKI: 1;

            

             A104: ((t |-- A) . ab) > 0

            proof

              (A \ {ab}) c= B1

              proof

                let x be object;

                assume x in (A \ {ab});

                then x in A & not x in {ab} by XBOOLE_0:def 5;

                hence thesis by A83, XBOOLE_0:def 5;

              end;

              then

               A105: ( conv (A \ {ab})) c= ( conv B1) by RLAFFIN1: 3;

              assume

               A106: ((t |-- A) . ab) <= 0 ;

              ((t |-- A) . ab) >= 0 by A7, A86, A102, RLAFFIN1: 71;

              then for x st x in {ab} holds ((t |-- A) . x) = 0 by A106, TARSKI:def 1;

              then t in ( conv (A \ {ab})) by A7, A86, A102, RLAFFIN1: 76;

              hence contradiction by A103, A105;

            end;

            

             A107: (BUU . t) = (1 / ( card U)) by A102, RLAFFIN2: 18;

            then t in ( Carrier BUU) by A102;

            then

            consider n be object such that

             A108: n in ( dom G) and

             A109: (G . n) = t by A92, FUNCT_1:def 3;

            reconsider n as Nat by A108;

            (F . n) = ((BUU . tt) * ((t |-- A) . ab)) by A93, A94, A108, A109;

            then 0 < ( Sum F) by A94, A96, A102, A104, A107, A108, RVSUM_1: 85;

            then

             A110: (((B . U) |-- A) . ab) > 0 by A85, A89, A90, RLAFFIN1:def 7;

            ( Carrier ((B . U) |-- BB)) c= BB by RLVECT_2:def 6;

            then

             A111: not ab in ( Carrier ((B . U) |-- BB)) by A83, A87, XBOOLE_0:def 5;

            ( conv BB) c= ( Affin BB) by RLAFFIN1: 65;

            then ((B . U) |-- A) = ((B . U) |-- BB) by A7, A81, A101, RLAFFIN1: 77;

            hence contradiction by A111, A110;

          end;

          then ( conv ( @ U)) c= ( conv B1) by CONVEX1: 30;

          then ( conv ( @ U)) misses ( Int A) by A79, RLAFFIN2: 7, XBOOLE_1: 63;

          then ( card XX) = 1 by A4, A44;

          then

          consider w1 be object such that

           A112: XX = {w1} by CARD_2: 42;

          w1 in XX by A112, TARSKI:def 1;

          then

          consider W1 be Simplex of n, K such that

           A113: w1 = W1 and

           A114: U c= W1;

          

           A115: (( card SS1) + Z) <= ( degree K) by A3, A16, A27, A30, A33, Th33;

          

           A116: X c= {(S \/ (B .: {W1}))}

          proof

            let x be object;

            

             A117: (n + 1) = (( degree K) + 1) by A3, XXREAL_3:def 2;

            assume x in X;

            then

            consider W be Simplex of n, ( BCS K) such that

             A118: x = W and

             A119: S c= W by A11;

            consider T be simplex-like finite Subset-Family of K such that

             A120: T misses SS1 and

             A121: (T \/ SS1) is c=-linear with_non-empty_elements and

             A122: ( card T) = (Z + 1) and

             A123: ( @ W) = ((B .: SS1) \/ (B .: T)) by A16, A36, A88, A115, A119, Th41;

            consider t be object such that

             A124: T = {t} by A122, CARD_2: 42;

            set TS = (T \/ SS1);

            

             A125: ( card TS) = (n + 1) by A16, A36, A120, A122, CARD_2: 40;

            

             A126: ( union TS) in TS by A121, A124, SIMPLEX0: 9;

            TS is simplex-like by TOPS_2: 13;

            then

            reconsider UTS = ( union TS) as Simplex of K by A126;

            ( Segm ( card TS)) c= ( Segm ( card UTS)) by A121, SIMPLEX0: 10;

            then

             A127: ( card TS) <= ( card UTS) by NAT_1: 39;

            UTS in T

            proof

              assume not UTS in T;

              then UTS in SS1 by A126, XBOOLE_0:def 3;

              then ( card UTS) <= ( card U) by NAT_1: 43, ZFMISC_1: 74;

              hence contradiction by A43, A125, A127, NAT_1: 13;

            end;

            then

             A128: UTS = t by A124, TARSKI:def 1;

            ( card UTS) <= (( degree K) + 1) by SIMPLEX0: 24;

            then ( card UTS) <= (n + 1) by A3, XXREAL_3:def 2;

            then ( card UTS) = (n + 1) & SS1 c= TS by A125, A127, XBOOLE_1: 7, XXREAL_0: 1;

            then U c= UTS & UTS is Simplex of n, K by A3, A117, SIMPLEX0:def 18, ZFMISC_1: 77;

            then UTS in XX;

            then W = ((B .: SS1) \/ (B .: {W1})) by A112, A113, A123, A124, A128, TARSKI:def 1;

            hence thesis by A35, A118, TARSKI:def 1;

          end;

          ( card W1) = (( degree K) + 1) by A3, SIMPLEX0:def 18;

          then ( card W1) = (n + 1) by A3, XXREAL_3:def 2;

          then { W where W be Simplex of n, ( BCS K) : S c= W & ( conv ( @ W)) c= ( conv ( @ W1)) } = {(S \/ (B .: {W1}))} by A16, A27, A30, A33, A36, A43, A114, Th42;

          then (S \/ (B .: {W1})) in { W where W be Simplex of n, ( BCS K) : S c= W & ( conv ( @ W)) c= ( conv ( @ W1)) } by TARSKI:def 1;

          then ex R be Simplex of n, ( BCS K) st R = (S \/ (B .: {W1})) & S c= R & ( conv ( @ R)) c= ( conv ( @ W1));

          then (S \/ (B .: {W1})) in X by A11;

          then X = {(S \/ (B .: {W1}))} by A116, ZFMISC_1: 33;

          hence ( card X) = 1 by CARD_1: 30;

        end;

          suppose

           A129: ( card U) = (n + 1);

          

           A130: ( conv ( @ S)) meets ( Int A)

          proof

            U is non empty by A129;

            then ( @ U) in ( dom B) by A31, ZFMISC_1: 56;

            then

             A131: S c= ( conv ( @ S)) & (B . U) in ( @ S) by A35, A38, FUNCT_1:def 6, RLAFFIN1: 2;

            then (B . U) in ( conv ( @ S));

            then

             A132: (B . U) in ( conv ( @ U)) by A42;

            set BUU = ((B . U) |-- ( @ U));

            assume

             A133: ( conv ( @ S)) misses ( Int A);

            ( conv ( @ S)) c= ( conv A) & A is non empty by A2, A41, A42;

            then

            consider BB be Subset of V such that

             A134: BB c< A and

             A135: ( conv ( @ S)) c= ( conv BB) by A7, A133, RLAFFIN2: 23;

            

             A136: BB c= A by A134;

            then

            reconsider B1 = BB as finite Subset of V;

            ( Affin ( @ S)) c= ( Affin BB) by A135, RLAFFIN1: 68;

            then

             A137: n <= ( card B1) by A16, RLAFFIN1: 79;

            

             A138: ( card B1) < (n + 1) by A2, A134, CARD_2: 48;

            then ( card B1) <= n by NAT_1: 13;

            then ( card B1) = n by A137, XXREAL_0: 1;

            then ( card (A \ BB)) = ((n + 1) - n) by A2, A136, CARD_2: 44;

            then

            consider ab be object such that

             A139: (A \ BB) = {ab} by CARD_2: 42;

            ( @ U) c= ( conv ( @ U)) by RLAFFIN1: 2;

            then

             A140: ( @ U) c= ( conv A) by A41;

            

             A141: ab in {ab} by TARSKI:def 1;

            then

            reconsider ab as Element of V by A139;

            

             A142: ( conv ( @ U)) c= ( Affin ( @ U)) by RLAFFIN1: 65;

            then ( sum BUU) = 1 by A132, RLAFFIN1:def 7;

            then

            consider F be FinSequence of REAL , G be FinSequence of the carrier of V such that

             A143: ((( Sum BUU) |-- A) . ab) = ( Sum F) and

             A144: ( len G) = ( len F) and G is one-to-one and

             A145: ( rng G) = ( Carrier BUU) and

             A146: for n st n in ( dom F) holds (F . n) = ((BUU . (G . n)) * (((G . n) |-- A) . ab)) by A7, A140, RLAFFIN2: 3;

            

             A147: ( dom G) = ( dom F) by A144, FINSEQ_3: 29;

            

             A148: (A \ {ab}) = (A /\ BB) by A139, XBOOLE_1: 48

            .= BB by A136, XBOOLE_1: 28;

            U c= ( conv B1)

            proof

              

               A149: ( Carrier BUU) c= U by RLVECT_2:def 6;

               A150:

              now

                let i be Nat such that

                 A151: i in ( dom F);

                

                 A152: (F . i) = ((BUU . (G . i)) * (((G . i) |-- A) . ab)) by A146, A151;

                

                 A153: (G . i) in ( rng G) by A147, A151, FUNCT_1:def 3;

                then (G . i) in U by A145, A149;

                then

                 A154: (((G . i) |-- A) . ab) >= 0 by A7, A140, RLAFFIN1: 71;

                (BUU . (G . i)) = (1 / ( card U)) by A145, A149, A153, RLAFFIN2: 18;

                hence 0 <= (F . i) by A152, A154;

              end;

              (B . U) in ( conv ( @ S)) by A131;

              then

               A155: (B . U) in ( conv BB) by A135;

              assume not U c= ( conv B1);

              then

              consider t be object such that

               A156: t in U and

               A157: not t in ( conv B1);

              reconsider tt = t as set by TARSKI: 1;

              U c= ( conv ( @ U)) by RLAFFIN1: 2;

              then

               A158: t in ( conv ( @ U)) by A156;

              

               A159: ((t |-- A) . ab) > 0

              proof

                assume

                 A160: ((t |-- A) . ab) <= 0 ;

                ((t |-- A) . ab) >= 0 by A7, A41, A158, RLAFFIN1: 71;

                then for y st y in (A \ B1) holds ((t |-- A) . y) = 0 by A139, A160, TARSKI:def 1;

                hence contradiction by A7, A41, A139, A148, A157, A158, RLAFFIN1: 76;

              end;

              

               A161: (BUU . t) = (1 / ( card U)) by A156, RLAFFIN2: 18;

              then t in ( Carrier BUU) by A156;

              then

              consider n be object such that

               A162: n in ( dom G) and

               A163: (G . n) = t by A145, FUNCT_1:def 3;

              reconsider n as Nat by A162;

              (F . n) = ((BUU . tt) * ((t |-- A) . ab)) by A146, A147, A162, A163;

              then 0 < ( Sum F) by A147, A150, A156, A159, A161, A162, RVSUM_1: 85;

              then

               A164: (((B . U) |-- A) . ab) > 0 by A132, A142, A143, RLAFFIN1:def 7;

              ( Carrier ((B . U) |-- BB)) c= BB by RLVECT_2:def 6;

              then

               A165: not ab in ( Carrier ((B . U) |-- BB)) by A139, A141, XBOOLE_0:def 5;

              ( conv BB) c= ( Affin BB) by RLAFFIN1: 65;

              then ((B . U) |-- A) = ((B . U) |-- BB) by A7, A136, A155, RLAFFIN1: 77;

              hence contradiction by A165, A164;

            end;

            then ( conv ( @ U)) c= ( conv B1) by CONVEX1: 30;

            then ( Affin ( @ U)) c= ( Affin B1) by RLAFFIN1: 68;

            hence contradiction by A129, A138, RLAFFIN1: 79;

          end;

          set XX = { S1 where S1 be Simplex of n, ( BCS K) : S c= S1 & ( conv ( @ S1)) c= ( conv ( @ U)) };

          

           A166: ( card XX) = 2 by A16, A30, A35, A36, A129, Th43;

          consider w1,w2 be object such that w1 <> w2 and

           A167: XX = {w1, w2} by A166, CARD_2: 60;

          w2 in XX by A167, TARSKI:def 2;

          then

          consider W2 be Simplex of n, ( BCS K) such that

           A168: w2 = W2 and

           A169: S c= W2 and ( conv ( @ W2)) c= ( conv ( @ U));

          w1 in XX by A167, TARSKI:def 2;

          then

          consider W1 be Simplex of n, ( BCS K) such that

           A170: w1 = W1 and

           A171: S c= W1 and ( conv ( @ W1)) c= ( conv ( @ U));

          

           A172: W1 in X by A11, A171;

          

           A173: X c= XX

          proof

            let w be object;

            assume w in X;

            then

            consider W be Simplex of n, ( BCS K) such that

             A174: w = W and

             A175: S c= W by A11;

            (( card SS1) + Z) <= ( degree K) by A3, A16, A27, A30, A33, Th33;

            then

            consider T be simplex-like finite Subset-Family of K such that T misses SS1 and

             A176: (T \/ SS1) is c=-linear with_non-empty_elements and ( card T) = (Z + 1) and

             A177: ( @ W) = ((B .: SS1) \/ (B .: T)) by A27, A30, A33, A34, A175, Th41;

            reconsider TS = (T \/ SS1) as finite simplex-like Subset-Family of K by TOPS_2: 13;

            

             A178: W = (B .: ( @ TS)) by A177, RELAT_1: 120;

            ( union TS) in TS by A37, A176, SIMPLEX0: 9;

            then

            reconsider UTS = ( union TS) as Simplex of K by TOPS_2:def 1;

            ( card UTS) <= (( degree K) + 1) by SIMPLEX0: 24;

            then

             A179: ( card UTS) <= (n + 1) by A3, XXREAL_3:def 2;

            

             A180: U c= ( union TS) by XBOOLE_1: 7, ZFMISC_1: 77;

            then (n + 1) <= ( card UTS) by A129, NAT_1: 43;

            then UTS = U by A129, A179, A180, CARD_2: 102, XXREAL_0: 1;

            then ( conv ( @ W)) c= ( conv ( @ U)) by A178, CONVEX1: 30, RLAFFIN2: 17;

            hence thesis by A174, A175;

          end;

          W2 in X by A11, A169;

          then XX c= X by A167, A170, A168, A172, ZFMISC_1: 32;

          hence thesis by A130, A166, A173, XBOOLE_0:def 10;

        end;

      end;

    end;

    theorem :: SIMPLEX1:45

    

     Th45: for S be Simplex of (n - 1), ( BCS (k,( Complex_of {Aff}))) st ( card Aff) = (n + 1) & X = { S1 where S1 be Simplex of n, ( BCS (k,( Complex_of {Aff}))) : S c= S1 } holds (( conv ( @ S)) meets ( Int Aff) implies ( card X) = 2) & (( conv ( @ S)) misses ( Int Aff) implies ( card X) = 1)

    proof

      let S be Simplex of (n - 1), ( BCS (k,( Complex_of {Aff}))) such that

       A1: ( card Aff) = (n + 1);

      set C = ( Complex_of {Aff});

      reconsider cA = ( card Aff) as ExtReal;

      

       A2: (cA - 1) = (( card Aff) + ( - 1)) by XXREAL_3:def 2

      .= n by A1;

      then

       A3: ( degree C) = n by SIMPLEX0: 26;

      defpred P[ Nat] means for S be Simplex of (n - 1), ( BCS ($1,C)), X be set st X = { S1 where S1 be Simplex of n, ( BCS ($1,C)) : S c= S1 } holds (( conv ( @ S)) meets ( Int Aff) implies ( card X) = 2) & (( conv ( @ S)) misses ( Int Aff) implies ( card X) = 1);

      

       A4: ( [#] C) = ( [#] V) & |.C.| c= ( [#] V);

      

       A5: P[ 0 qua Nat]

      proof

        reconsider n1 = (n - 1) as ExtReal;

        

         A6: the topology of C = ( bool Aff) by SIMPLEX0: 4;

        Aff in ( bool Aff) by ZFMISC_1:def 1;

        then

        reconsider A1 = Aff as finite Simplex of C by A6, PRE_TOPC:def 2;

        

         A7: ( BCS ( 0 ,C)) = C by A4, Th16;

        let S be Simplex of (n - 1), ( BCS ( 0 ,C)), X be set such that

         A8: X = { S1 where S1 be Simplex of n, ( BCS ( 0 ,C)) : S c= S1 };

        

         A9: X c= {Aff}

        proof

          let x be object;

          reconsider N = n as ExtReal;

          assume x in X;

          then

          consider U be Simplex of n, C such that

           A10: x = U and S c= U by A7, A8;

          

           A11: U in the topology of C by PRE_TOPC:def 2;

          ( card U) = (N + 1) by A3, SIMPLEX0:def 18

          .= (n + 1) by XXREAL_3:def 2;

          then Aff = U by A1, A6, A11, CARD_2: 102;

          hence thesis by A10, TARSKI:def 1;

        end;

        

         A12: S in ( bool Aff) by A6, A7, PRE_TOPC:def 2;

        A1 is Simplex of n, C by A2, SIMPLEX0: 48;

        then Aff in X by A7, A8, A12;

        then

         A13: X = {Aff} by A9, ZFMISC_1: 33;

        (n + ( - 1)) >= ( - 1) & (n - 1) <= ( degree C) by A3, XREAL_1: 31, XREAL_1: 146;

        

        then ( card S) = (n1 + 1) by A7, SIMPLEX0:def 18

        .= ((n - 1) + 1) by XXREAL_3:def 2;

        then S <> Aff by A1;

        then S c< Aff by A12;

        hence thesis by A13, CARD_1: 30, RLAFFIN2: 7;

      end;

      

       A14: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A15: P[k];

        

         A16: ( degree ( BCS (k,C))) = n & ( BCS ((k + 1),C)) = ( BCS ( BCS (k,C))) by A3, A4, Th20, Th32;

        let S be Simplex of (n - 1), ( BCS ((k + 1),C)), X such that

         A17: X = { S1 where S1 be Simplex of n, ( BCS ((k + 1),C)) : S c= S1 };

        thus thesis by A1, A15, A16, A17, Th44;

      end;

      for k holds P[k] from NAT_1:sch 2( A5, A14);

      hence thesis;

    end;

    begin

    reserve v for Vertex of ( BCS (k,( Complex_of {Aff}))),

F for Function of ( Vertices ( BCS (k,( Complex_of {Aff})))), Aff;

    theorem :: SIMPLEX1:46

    

     Th46: for F st for v, B st B c= Aff & v in ( conv B) holds (F . v) in B holds ex n st ( card { S where S be Simplex of (( card Aff) - 1), ( BCS (k,( Complex_of {Aff}))) : (F .: S) = Aff }) = ((2 * n) + 1)

    proof

      reconsider O = 1 as ExtReal;

      reconsider Z = 0 as ExtReal;

      defpred P[ Nat] means for A be finite affinely-independent Subset of V st ( card A) = $1 holds for F be Function of ( Vertices ( BCS (k,( Complex_of {A})))), A st for v be Vertex of ( BCS (k,( Complex_of {A}))) holds for B be Subset of V st B c= A & v in ( conv B) holds (F . v) in B holds ex n st ( card { S where S be Simplex of (( card A) - 1), ( BCS (k,( Complex_of {A}))) : (F .: S) = A }) = ((2 * n) + 1);

      

       A1: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat such that

         A2: P[m];

        let A be finite affinely-independent Subset of V such that

         A3: ( card A) = (m + 1);

        A is non empty by A3;

        then

        consider a be object such that

         A4: a in A;

        reconsider a as Element of V by A4;

        

         A5: ( card (A \ {a})) = m by A3, A4, STIRL2_1: 55;

        reconsider Aa = (A \ {a}) as finite affinely-independent Subset of V by RLAFFIN1: 43, XBOOLE_1: 36;

        set CAa = ( Complex_of {Aa});

        the topology of CAa = ( bool Aa) by SIMPLEX0: 4;

        

        then

         A6: ( Vertices CAa) = ( union ( bool Aa)) by SIMPLEX0: 16

        .= Aa by ZFMISC_1: 81;

        

         A7: ( [#] CAa) = ( [#] V) & |.CAa.| c= ( [#] V);

        then

         A8: ( Vertices CAa) c= ( Vertices ( BCS (k,CAa))) by Th24;

        set CA = ( Complex_of {A});

        let F be Function of ( Vertices ( BCS (k,CA))), A such that

         A9: for v be Vertex of ( BCS (k,CA)) holds for B be Subset of V st B c= A & v in ( conv B) holds (F . v) in B;

        set XX = { S where S be Simplex of (( card A) - 1), ( BCS (k,CA)) : (F .: S) = A };

        

         A10: XX c= the topology of ( BCS (k,CA))

        proof

          let x be object;

          assume x in XX;

          then ex S be Simplex of (( card A) - 1), ( BCS (k,CA)) st S = x & A = (F .: S);

          hence thesis by PRE_TOPC:def 2;

        end;

        then

        reconsider XX as Subset-Family of ( BCS (k,CA)) by XBOOLE_1: 1;

        reconsider XX as simplex-like Subset-Family of ( BCS (k,CA)) by A10, SIMPLEX0: 14;

        

         A11: ( [#] CA) = ( [#] V) & |.CA.| c= ( [#] V);

        

         A12: (A \ {a}) c= A by XBOOLE_1: 36;

        for x st x in {Aa} holds ex y st y in {A} & x c= y

        proof

          let x;

          assume

           A13: x in {Aa};

          take A;

          thus thesis by A12, A13, TARSKI:def 1;

        end;

        then {Aa} is_finer_than {A};

        then CAa is SubSimplicialComplex of CA by SIMPLEX0: 30;

        then

         A14: ( BCS (k,CAa)) is SubSimplicialComplex of ( BCS (k,CA)) by A11, A7, Th23;

        then

         A15: ( Vertices ( BCS (k,CAa))) c= ( Vertices ( BCS (k,CA))) by SIMPLEX0: 31;

        

         A16: the topology of CA = ( bool A) by SIMPLEX0: 4;

        

        then

         A17: ( Vertices CA) = ( union ( bool A)) by SIMPLEX0: 16

        .= A by ZFMISC_1: 81;

        

         A18: ( dom F) = ( Vertices ( BCS (k,CA))) by A4, FUNCT_2:def 1;

        per cases ;

          suppose

           A19: m = 0 ;

          

           A20: (O - 1) = 0 by XXREAL_3: 7;

          then

           A21: ( degree CA) = 0 by A3, A19, SIMPLEX0: 26;

          k = 0 or k > 0 ;

          then

           A22: ( BCS (k,CA)) = CA by A11, A21, Th16, Th22;

          then

           A23: ( dom F) = ( Vertices CA) by A4, FUNCT_2:def 1;

          take 0 ;

          A in ( bool A) by ZFMISC_1:def 1;

          then

          reconsider A1 = A as Simplex of CA by A16, PRE_TOPC:def 2;

          

           A24: A1 is Simplex of 0 , CA by A3, A19, A20, SIMPLEX0: 48;

          ex x be object st A = {x} by A3, A19, CARD_2: 42;

          then

           A25: A = {a} by A4, TARSKI:def 1;

          then ( conv A) = A by RLAFFIN1: 1;

          then (F . a) in A by A4, A9, A17, A22;

          then

           A26: (F . a) = a by A25, TARSKI:def 1;

          

           A27: XX c= {A}

          proof

            let x be object;

            assume x in XX;

            then

            consider S be Simplex of 0 , CA such that

             A28: x = S and (F .: S) = A by A3, A19, A22;

            

             A29: S in the topology of CA by PRE_TOPC:def 2;

            ( card S) = (Z + 1) by A21, SIMPLEX0:def 18

            .= 1 by XXREAL_3: 4;

            then S = A by A3, A16, A19, A29, CARD_2: 102;

            hence thesis by A28, TARSKI:def 1;

          end;

          (F .: A) = ( Im (F,a)) by A25, RELAT_1:def 16

          .= A by A4, A17, A23, A25, A26, FUNCT_1: 59;

          then A in XX by A3, A19, A24, A22;

          then XX = {A} by A27, ZFMISC_1: 33;

          hence thesis by CARD_1: 30;

        end;

          suppose

           A30: m > 0 ;

          defpred P[ object, object] means ex D1,D2 be set st D1 = $1 & D2 = $2 & D1 c= D2;

          set XXA = { S where S be Simplex of (m - 1), ( BCS (k,CA)) : (F .: S) = Aa & ( conv ( @ S)) misses ( Int A) };

          reconsider m1 = (m - 1) as ExtReal;

          reconsider M = m as ExtReal;

          reconsider cA = ( card A) as ExtReal;

          set YA = { S where S be Simplex of m, ( BCS (k,CA)) : Aa = (F .: S) };

          

           A31: YA c= the topology of ( BCS (k,CA))

          proof

            let x be object;

            assume x in YA;

            then ex S be Simplex of m, ( BCS (k,CA)) st S = x & Aa = (F .: S);

            hence thesis by PRE_TOPC:def 2;

          end;

          then

          reconsider YA as Subset-Family of ( BCS (k,CA)) by XBOOLE_1: 1;

          reconsider YA as simplex-like Subset-Family of ( BCS (k,CA)) by A31, SIMPLEX0: 14;

          defpred P1[ object, object] means ex D1,D2 be set st D1 = $1 & D2 = $2 & D2 c= D1;

          set Xm1 = { S where S be Simplex of (m - 1), ( BCS (k,CA)) : Aa = (F .: S) };

          set Xm = the set of all S where S be Simplex of m, ( BCS (k,CA));

          consider R1 be Relation such that

           A32: for x,y be object holds [x, y] in R1 iff x in Xm & y in Xm1 & P1[x, y] from RELAT_1:sch 1;

          set DY = (( dom R1) \ YA);

          

           A33: DY c= XX

          proof

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            assume

             A34: x in DY;

            then

            consider y be object such that

             A35: [x, y] in R1 by XTUPLE_0:def 12;

            reconsider yy = y as set by TARSKI: 1;

            x in Xm by A32, A35;

            then

            consider S be Simplex of m, ( BCS (k,CA)) such that

             A36: x = S and not contradiction;

             not x in YA by A34, XBOOLE_0:def 5;

            then

             A37: (F .: S) <> Aa by A36;

            y in Xm1 by A32, A35;

            then

             A38: ex W be Simplex of (m - 1), ( BCS (k,CA)) st y = W & Aa = (F .: W);

             P1[xx, yy] by A32, A35;

            then yy c= xx;

            then Aa c= (F .: S) by A36, A38, RELAT_1: 123;

            then Aa c< (F .: S) by A37;

            then m < ( card (F .: S)) by A5, CARD_2: 48;

            then

             A39: (m + 1) <= ( card (F .: S)) by NAT_1: 13;

            ( card (F .: S)) <= (m + 1) by A3, NAT_1: 43;

            then (F .: S) = A by A3, A39, CARD_2: 102, XXREAL_0: 1;

            hence thesis by A3, A36;

          end;

          set RDY = (R1 | DY);

          

           A40: (RDY | (( dom RDY) \ DY)) = {}

          proof

            assume (RDY | (( dom RDY) \ DY)) <> {} ;

            then

            consider xy be object such that

             A41: xy in (RDY | (( dom RDY) \ DY)) by XBOOLE_0:def 1;

            consider x,y be object such that

             A42: xy = [x, y] by A41, RELAT_1:def 1;

            

             A43: x in (( dom RDY) \ DY) by A41, A42, RELAT_1:def 11;

            then ( dom RDY) c= DY & x in ( dom RDY) by RELAT_1: 58;

            hence contradiction by A43, XBOOLE_0:def 5;

          end;

          

           A44: (2 *` ( card YA)) = (( card 2) *` ( card ( card YA)))

          .= ( card (2 * ( card YA))) by CARD_2: 39;

          (cA - 1) = ((m + 1) + ( - 1)) by A3, XXREAL_3:def 2;

          then

           A45: ( degree CA) = m by SIMPLEX0: 26;

          consider R be Relation such that

           A46: for x,y be object holds [x, y] in R iff x in Xm1 & y in Xm & P[x, y] from RELAT_1:sch 1;

          

           A47: ( card R) = ( card R1)

          proof

            deffunc F( object) = [($1 `2 ), ($1 `1 )];

            

             A48: for x be object st x in R holds F(x) in R1

            proof

              let z be object;

              assume

               A49: z in R;

              then ex x,y be object st z = [x, y] by RELAT_1:def 1;

              then

               A50: z = [(z `1 ), (z `2 )];

              then

               A51: (z `2 ) in Xm by A46, A49;

               P[(z `1 ), (z `2 )] & (z `1 ) in Xm1 by A46, A49, A50;

              hence thesis by A32, A51;

            end;

            consider f be Function of R, R1 such that

             A52: for x be object st x in R holds (f . x) = F(x) from FUNCT_2:sch 2( A48);

            per cases ;

              suppose

               A53: R1 is empty;

              R is empty by A48, A53;

              hence thesis by A53;

            end;

              suppose R1 is non empty;

              then

               A54: ( dom f) = R by FUNCT_2:def 1;

              R1 c= ( rng f)

              proof

                let z be object;

                assume

                 A55: z in R1;

                then ex x,y be object st z = [x, y] by RELAT_1:def 1;

                then

                 A56: z = [(z `1 ), (z `2 )];

                then

                 A57: (z `2 ) in Xm1 by A32, A55;

                 P1[(z `1 ), (z `2 )] & (z `1 ) in Xm by A32, A55, A56;

                then

                 A58: [(z `2 ), (z `1 )] in R by A46, A57;

                 F([) = z by A56;

                then z = (f . [(z `2 ), (z `1 )]) by A52, A58;

                hence thesis by A54, A58, FUNCT_1:def 3;

              end;

              then

               A59: ( rng f) = R1;

              now

                let x1,x2 be object such that

                 A60: x1 in R and

                 A61: x2 in R and

                 A62: (f . x1) = (f . x2);

                (f . x1) = F(x1) & (f . x2) = F(x2) by A52, A60, A61;

                then

                 A63: (x1 `2 ) = (x2 `2 ) & (x1 `1 ) = (x2 `1 ) by A62, XTUPLE_0: 1;

                

                 A64: ex x,y be object st x2 = [x, y] by A61, RELAT_1:def 1;

                ex x,y be object st x1 = [x, y] by A60, RELAT_1:def 1;

                

                hence x1 = [(x2 `1 ), (x2 `2 )] by A63

                .= x2 by A64;

              end;

              then f is one-to-one by A54, FUNCT_1:def 4;

              then (R,R1) are_equipotent by A54, A59, WELLORD2:def 4;

              hence thesis by CARD_1: 5;

            end;

          end;

          

           A65: |.( BCS (k,CAa)).| = |.CAa.| & |.CAa.| = ( conv Aa) by Th8, Th10;

          set DX = (( dom R) \ XXA);

          

           A66: DX c= the topology of ( BCS (k,CA))

          proof

            let x be object;

            assume x in DX;

            then ex y be object st [x, y] in R by XTUPLE_0:def 12;

            then x in Xm1 by A46;

            then ex S be Simplex of (m - 1), ( BCS (k,CA)) st S = x & Aa = (F .: S);

            hence thesis by PRE_TOPC:def 2;

          end;

          set RDX = (R | DX);

          reconsider DX as Subset-Family of ( BCS (k,CA)) by A66, XBOOLE_1: 1;

          reconsider DX as simplex-like Subset-Family of ( BCS (k,CA)) by A66, SIMPLEX0: 14;

          

           A67: (RDX | (( dom RDX) \ DX)) = {}

          proof

            assume (RDX | (( dom RDX) \ DX)) <> {} ;

            then

            consider xy be object such that

             A68: xy in (RDX | (( dom RDX) \ DX)) by XBOOLE_0:def 1;

            consider x,y be object such that

             A69: xy = [x, y] by A68, RELAT_1:def 1;

            

             A70: x in (( dom RDX) \ DX) by A68, A69, RELAT_1:def 11;

            then ( dom RDX) c= DX & x in ( dom RDX) by RELAT_1: 58;

            hence contradiction by A70, XBOOLE_0:def 5;

          end;

          

           A71: (m1 + 1) = ((m - 1) + 1) by XXREAL_3:def 2

          .= m;

          set FA = (F | ( Vertices ( BCS (k,CAa))));

          

           A72: ( dom FA) = ( Vertices ( BCS (k,CAa))) by A18, A14, RELAT_1: 62, SIMPLEX0: 31;

          

           A73: ( Vertices ( BCS (k,CAa))) is non empty by A5, A6, A8, A30;

          

           A74: for v be Vertex of ( BCS (k,CAa)) holds for B be Subset of V st B c= Aa & v in ( conv B) holds (FA . v) in B

          proof

            let v be Vertex of ( BCS (k,CAa));

            let B be Subset of V;

            assume

             A75: B c= Aa & v in ( conv B);

            v in ( Vertices ( BCS (k,CAa))) by A73;

            then (F . v) in B by A9, A12, A15, A75, XBOOLE_1: 1;

            hence thesis by A72, A73, FUNCT_1: 47;

          end;

          ( rng FA) c= Aa

          proof

            let y be object;

            assume y in ( rng FA);

            then

            consider x be object such that

             A76: x in ( dom FA) and

             A77: (FA . x) = y by FUNCT_1:def 3;

            reconsider v = x as Element of ( BCS (k,CAa)) by A72, A76;

            v is vertex-like by A72, A76, SIMPLEX0:def 4;

            then

            consider S be Subset of ( BCS (k,CAa)) such that

             A78: S is simplex-like and

             A79: v in S;

            

             A80: ( conv ( @ S)) c= |.( BCS (k,CAa)).| by A78, Th5;

            S c= ( conv ( @ S)) by RLAFFIN1: 2;

            then

             A81: v in ( conv ( @ S)) by A79;

            x in ( Vertices ( BCS (k,CAa))) by A18, A14, A76, RELAT_1: 62, SIMPLEX0: 31;

            hence thesis by A65, A74, A77, A80, A81;

          end;

          then

          reconsider FA as Function of ( Vertices ( BCS (k,CAa))), Aa by A72, FUNCT_2: 2;

          set XXa = { S where S be Simplex of (m - 1), ( BCS (k,CAa)) : (FA .: S) = Aa };

          consider n such that

           A82: ( card XXa) = ((2 * n) + 1) by A2, A5, A74;

          

           A83: (m - 1) <= (m - 0 ) & ( - 1) <= (m + ( - 1)) by XREAL_1: 10, XREAL_1: 31;

          

           A84: for x be object st x in XXA holds ( card ( Im (R,x))) = 1

          proof

            let x be object;

            assume x in XXA;

            then

            consider S be Simplex of (m - 1), ( BCS (k,CA)) such that

             A85: x = S and

             A86: (F .: S) = Aa and

             A87: ( conv ( @ S)) misses ( Int A);

            set XX = { S1 where S1 be Simplex of m, ( BCS (k,CA)) : S c= S1 };

            

             A88: (R .: {S}) c= XX

            proof

              let w be object;

              reconsider ww = w as set by TARSKI: 1;

              assume w in (R .: {S});

              then

              consider s be object such that

               A89: [s, w] in R and

               A90: s in {S} by RELAT_1:def 13;

              reconsider ss = s as set by TARSKI: 1;

              w in Xm by A46, A89;

              then

               A91: ex W be Simplex of m, ( BCS (k,CA)) st w = W;

               P[ss, ww] by A46, A89;

              then s = S & ss c= ww by A90, TARSKI:def 1;

              hence thesis by A91;

            end;

            XX c= (R .: {S})

            proof

              let w be object;

              assume w in XX;

              then

              consider W be Simplex of m, ( BCS (k,CA)) such that

               A92: w = W and

               A93: S c= W;

              W in Xm & S in Xm1 by A86;

              then S in {S} & [S, W] in R by A46, A93, TARSKI:def 1;

              hence thesis by A92, RELAT_1:def 13;

            end;

            then

             A94: (R .: {S}) = XX by A88;

            ( card XX) = 1 by A3, A87, Th45;

            hence thesis by A85, A94, RELAT_1:def 16;

          end;

          

           A95: ( degree CA) = ( degree ( BCS (k,CA))) by A11, Th32;

          

           A96: (M + 1) = (m + 1) by XXREAL_3:def 2;

          

           A97: for x be object st x in YA holds ( card ( Im (R1,x))) = 2

          proof

            let x be object;

            assume x in YA;

            then

            consider S be Simplex of m, ( BCS (k,CA)) such that

             A98: x = S and

             A99: Aa = (F .: S);

            set FS = (F | S);

            

             A100: ( rng FS) = Aa by A99, RELAT_1: 115;

            

             A101: Aa is non empty by A5, A30;

            

             A102: S in {x} by A98, TARSKI:def 1;

            

             A103: ( dom FS) = S by A18, RELAT_1: 62, SIMPLEX0: 17;

            

             A104: ( card S) = (m + 1) by A95, A45, A96, SIMPLEX0:def 18;

            reconsider FS as Function of S, Aa by A100, A103, FUNCT_2: 1;

            FS is onto by A100, FUNCT_2:def 3;

            then

            consider b be set such that

             A105: b in Aa and

             A106: ( card (FS " {b})) = 2 and

             A107: for x st x in Aa & x <> b holds ( card (FS " {x})) = 1 by A5, A101, A104, Th2;

            consider a1,a2 be object such that

             A108: a1 <> a2 and

             A109: (FS " {b}) = {a1, a2} by A106, CARD_2: 60;

            reconsider S1 = (S \ {a1}), S2 = (S \ {a2}) as Simplex of ( BCS (k,CA));

            

             A110: a1 in {a1, a2} by TARSKI:def 2;

            then

             A111: a1 in S2 by A108, A109, ZFMISC_1: 56;

            

             A112: ( card S1) = m by A104, A109, A110, STIRL2_1: 55;

            

             A113: a2 in {a1, a2} by TARSKI:def 2;

            then

             A114: ( card S2) = m by A104, A109, STIRL2_1: 55;

            then

            reconsider S1, S2 as Simplex of (m - 1), ( BCS (k,CA)) by A95, A83, A71, A45, A112, SIMPLEX0:def 18;

            

             A115: {a1} c= S by A109, A110, ZFMISC_1: 31;

            

             A116: (FS . a2) = (F . a2) by A103, A109, A113, FUNCT_1: 47;

            

             A117: {a2} c= S by A109, A113, ZFMISC_1: 31;

            

             A118: (R1 .: {x}) c= {S1, S2}

            proof

              let Y be object;

              assume Y in (R1 .: {x});

              then

              consider X be object such that

               A119: [X, Y] in R1 and

               A120: X in {x} by RELAT_1:def 13;

              Y in Xm1 by A32, A119;

              then

              consider W be Simplex of (m - 1), ( BCS (k,CA)) such that

               A121: Y = W and

               A122: Aa = (F .: W);

              X = x by A120, TARSKI:def 1;

              then P1[S, W] by A32, A98, A119, A121;

              then W c= S;

              then

               A123: Aa = (FS .: W) by A122, RELAT_1: 129;

              then

              consider w be object such that

               A124: w in ( dom FS) and

               A125: w in W and

               A126: (FS . w) = b by A105, FUNCT_1:def 6;

              

               A127: {w} c= W by A125, ZFMISC_1: 31;

              

               A128: (S \ {a1, a2}) c= W

              proof

                let s be object;

                assume

                 A129: s in (S \ {a1, a2});

                then

                 A130: s in ( dom FS) by A103, XBOOLE_0:def 5;

                then

                 A131: (FS . s) in Aa by A100, FUNCT_1:def 3;

                then

                consider w be object such that

                 A132: w in ( dom FS) and

                 A133: w in W and

                 A134: (FS . w) = (FS . s) by A123, FUNCT_1:def 6;

                 not s in (FS " {b}) by A109, A129, XBOOLE_0:def 5;

                then not (FS . s) in {b} by A130, FUNCT_1:def 7;

                then (FS . s) <> b by TARSKI:def 1;

                then ( card (FS " {(FS . s)})) = 1 by A107, A131;

                then

                consider z be object such that

                 A135: (FS " {(FS . s)}) = {z} by CARD_2: 42;

                

                 A136: (FS . s) in {(FS . s)} by TARSKI:def 1;

                then

                 A137: s in (FS " {(FS . s)}) by A130, FUNCT_1:def 7;

                w in (FS " {(FS . s)}) by A132, A134, A136, FUNCT_1:def 7;

                then w = z by A135, TARSKI:def 1;

                hence thesis by A133, A135, A137, TARSKI:def 1;

              end;

              b in {b} by TARSKI:def 1;

              then

               A138: w in (FS " {b}) by A124, A126, FUNCT_1:def 7;

              

               A139: ( card W) = m by A95, A83, A71, A45, SIMPLEX0:def 18;

              

               A140: (S /\ {a1}) = {a1} by A115, XBOOLE_1: 28;

              

               A141: (S /\ {a2}) = {a2} by A117, XBOOLE_1: 28;

              per cases by A109, A138, TARSKI:def 2;

                suppose w = a1;

                

                then ((S \ {a1, a2}) \/ {w}) = (S \ ( {a1, a2} \ {a1})) by A140, XBOOLE_1: 52

                .= S2 by A108, ZFMISC_1: 17;

                then S2 = W by A114, A127, A128, A139, CARD_2: 102, XBOOLE_1: 8;

                hence thesis by A121, TARSKI:def 2;

              end;

                suppose w = a2;

                

                then ((S \ {a1, a2}) \/ {w}) = (S \ ( {a1, a2} \ {a2})) by A141, XBOOLE_1: 52

                .= S1 by A108, ZFMISC_1: 17;

                then S1 = W by A112, A127, A128, A139, CARD_2: 102, XBOOLE_1: 8;

                hence thesis by A121, TARSKI:def 2;

              end;

            end;

            

             A142: S c= ( dom F) by A18, SIMPLEX0: 17;

            

             A143: (FS . a1) = (F . a1) by A103, A109, A110, FUNCT_1: 47;

            

             A144: (FS . a1) in {b} by A109, A110, FUNCT_1:def 7;

            then

             A145: (FS . a1) = b by TARSKI:def 1;

            

             A146: (FS . a2) in {b} by A109, A113, FUNCT_1:def 7;

            then

             A147: (FS . a2) = b by TARSKI:def 1;

            

             A148: a2 in S & a2 in S1 by A108, A109, A113, ZFMISC_1: 56;

            

             A149: Aa c= (F .: S1)

            proof

              let z be object;

              assume

               A150: z in Aa;

              per cases ;

                suppose

                 A151: z = b;

                (FS . a2) in (F .: S1) by A142, A116, A148, FUNCT_1:def 6;

                hence thesis by A146, A151, TARSKI:def 1;

              end;

                suppose

                 A152: z <> b;

                consider c be object such that

                 A153: c in ( dom F) and

                 A154: c in S and

                 A155: z = (F . c) by A99, A150, FUNCT_1:def 6;

                c in S1 by A143, A145, A152, A154, A155, ZFMISC_1: 56;

                hence thesis by A153, A155, FUNCT_1:def 6;

              end;

            end;

            

             A156: S in Xm;

            

             A157: a1 in S & a1 in S2 by A108, A109, A110, ZFMISC_1: 56;

            

             A158: Aa c= (F .: S2)

            proof

              let z be object;

              assume

               A159: z in Aa;

              per cases ;

                suppose

                 A160: z = b;

                (FS . a1) in (F .: S2) by A143, A142, A157, FUNCT_1:def 6;

                hence thesis by A144, A160, TARSKI:def 1;

              end;

                suppose

                 A161: z <> b;

                consider c be object such that

                 A162: c in ( dom F) and

                 A163: c in S and

                 A164: z = (F . c) by A99, A159, FUNCT_1:def 6;

                c in S2 by A116, A147, A161, A163, A164, ZFMISC_1: 56;

                hence thesis by A162, A164, FUNCT_1:def 6;

              end;

            end;

            (F .: S1) c= Aa by A99, RELAT_1: 123, XBOOLE_1: 36;

            then Aa = (F .: S1) by A149;

            then (S \ {a1}) c= S & S1 in Xm1 by XBOOLE_1: 36;

            then [S, S1] in R1 by A32, A156;

            then

             A165: S1 in (R1 .: {x}) by A102, RELAT_1:def 13;

            (F .: S2) c= Aa by A99, RELAT_1: 123, XBOOLE_1: 36;

            then Aa = (F .: S2) by A158;

            then (S \ {a2}) c= S & S2 in Xm1 by XBOOLE_1: 36;

            then [S, S2] in R1 by A32, A156;

            then S2 in (R1 .: {x}) by A102, RELAT_1:def 13;

            then {S1, S2} c= (R1 .: {x}) by A165, ZFMISC_1: 32;

            then

             A166: (R1 .: {x}) = {S1, S2} by A118;

            S1 <> S2 by A111, ZFMISC_1: 56;

            then ( card (R1 .: {x})) = 2 by A166, CARD_2: 57;

            hence thesis by RELAT_1:def 16;

          end;

          

           A167: (M - 1) = (m + ( - 1)) by XXREAL_3:def 2;

          XX c= DY

          proof

            let x be object;

            assume x in XX;

            then

            consider S be Simplex of m, ( BCS (k,CA)) such that

             A168: x = S and

             A169: (F .: S) = A by A3;

            set FS = (F | S);

            

             A170: ( rng FS) = A by A169, RELAT_1: 115;

            

             A171: ( card A) = ( card S) by A3, A95, A45, A96, SIMPLEX0:def 18;

            

             A172: ( dom FS) = S by A18, RELAT_1: 62, SIMPLEX0: 17;

            then

            reconsider FS as Function of S, A by A170, FUNCT_2: 1;

            consider s be object such that

             A173: s in ( dom FS) & (FS . s) = a by A4, A170, FUNCT_1:def 3;

            set Ss = (S \ {s});

            FS is onto by A170, FUNCT_2:def 3;

            then

             A174: FS is one-to-one by A171, FINSEQ_4: 63;

            

            then

             A175: (FS .: Ss) = ((FS .: S) \ (FS .: {s})) by FUNCT_1: 64

            .= (A \ (FS .: {s})) by A170, A172, RELAT_1: 113

            .= (A \ ( Im (FS,s))) by RELAT_1:def 16

            .= Aa by A173, FUNCT_1: 59;

            (Ss,(FS .: Ss)) are_equipotent by A172, A174, CARD_1: 33, XBOOLE_1: 36;

            then

             A176: ( card Ss) = m by A5, A175, CARD_1: 5;

            reconsider Ss as Simplex of ( BCS (k,CA));

            reconsider Ss as Simplex of (m - 1), ( BCS (k,CA)) by A167, A176, SIMPLEX0: 48;

            (FS .: Ss) = (F .: Ss) by RELAT_1: 129, XBOOLE_1: 36;

            then

             A177: Ss in Xm1 by A175;

            Ss c= S & S in Xm by XBOOLE_1: 36;

            then [S, Ss] in R1 by A32, A177;

            then

             A178: S in ( dom R1) by XTUPLE_0:def 12;

            for W be Simplex of m, ( BCS (k,CA)) st S = W holds Aa <> (F .: W) by A4, A169, ZFMISC_1: 56;

            then not S in YA;

            hence thesis by A168, A178, XBOOLE_0:def 5;

          end;

          then

           A179: DY = XX by A33;

          for x be object st x in DY holds ( card ( Im (RDY,x))) = 1

          proof

            let x be object;

            assume

             A180: x in DY;

            then

            consider y be object such that

             A181: [x, y] in R1 by XTUPLE_0:def 12;

            

             A182: ex W be Simplex of m, ( BCS (k,CA)) st x = W & (F .: W) = A by A3, A179, A180;

            x in Xm by A32, A181;

            then

            consider S be Simplex of m, ( BCS (k,CA)) such that

             A183: x = S and not contradiction;

            y in Xm1 by A32, A181;

            then

            consider W be Simplex of (m - 1), ( BCS (k,CA)) such that

             A184: y = W and

             A185: Aa = (F .: W);

            

             A186: ( card S) = (m + 1) by A95, A45, A96, SIMPLEX0:def 18;

            

             A187: (RDY .: {x}) c= {y}

            proof

              let u be object;

              set FS = (F | S);

              assume u in (RDY .: {x});

              then

              consider s be object such that

               A188: [s, u] in RDY and

               A189: s in {x} by RELAT_1:def 13;

              

               A190: [s, u] in R1 by A188, RELAT_1:def 11;

              then u in Xm1 by A32;

              then

              consider U be Simplex of (m - 1), ( BCS (k,CA)) such that

               A191: u = U and

               A192: Aa = (F .: U);

              

               A193: ( dom FS) = S by A18, RELAT_1: 62, SIMPLEX0: 17;

              

               A194: ( rng FS) = A by A182, A183, RELAT_1: 115;

              then

              reconsider FS as Function of S, A by A193, FUNCT_2: 1;

               P1[S, W] by A32, A181, A183, A184;

              then

               A195: W c= S;

              then

               A196: (FS .: W) = (F .: W) by RELAT_1: 129;

              s = S by A183, A189, TARSKI:def 1;

              then P1[S, U] by A32, A190, A191;

              then

               A197: U c= S;

              then

               A198: (FS .: U) = (F .: U) by RELAT_1: 129;

              FS is onto by A194, FUNCT_2:def 3;

              then

               A199: FS is one-to-one by A3, A186, FINSEQ_4: 63;

              then

               A200: U c= W by A185, A192, A193, A196, A197, A198, FUNCT_1: 87;

              W c= U by A185, A192, A193, A195, A196, A198, A199, FUNCT_1: 87;

              then u = y by A184, A191, A200, XBOOLE_0:def 10;

              hence thesis by TARSKI:def 1;

            end;

            x in {x} & [x, y] in RDY by A180, A181, RELAT_1:def 11, TARSKI:def 1;

            then y in (RDY .: {x}) by RELAT_1:def 13;

            then (RDY .: {x}) = {y} by A187, ZFMISC_1: 33;

            then ( Im (RDY,x)) = {y} by RELAT_1:def 16;

            hence thesis by CARD_1: 30;

          end;

          

          then ( card RDY) = (( card {} ) +` (1 *` ( card DY))) by A40, Th1

          .= (1 *` ( card DY)) by CARD_2: 18

          .= ( card DY) by CARD_2: 21;

          

          then

           A201: ( card R1) = (( card ( card XX)) +` ( card (2 * ( card YA)))) by A44, A97, A179, Th1

          .= ( card (( card XX) + (2 * ( card YA)))) by CARD_2: 38

          .= (( card XX) + (2 * ( card YA)));

          

           A202: |.( BCS (k,CA)).| = |.CA.| & |.CA.| = ( conv A) by Th8, Th10;

          

           A203: XXA c= XXa

          proof

            let x be object;

            assume x in XXA;

            then

            consider S be Simplex of (m - 1), ( BCS (k,CA)) such that

             A204: x = S and

             A205: (F .: S) = Aa and

             A206: ( conv ( @ S)) misses ( Int A);

            ( conv ( @ S)) c= ( conv A) by A202, Th5;

            then

            consider B be Subset of V such that

             A207: B c< A and

             A208: ( conv ( @ S)) c= ( conv B) by A4, A206, RLAFFIN2: 23;

            

             A209: B c= A by A207;

            then

            reconsider B as finite Subset of V;

            ( card B) < (m + 1) by A3, A207, CARD_2: 48;

            then

             A210: ( card B) <= m by NAT_1: 13;

            

             A211: Aa c= B

            proof

              let y be object;

              assume y in Aa;

              then

              consider v be object such that

               A212: v in ( dom F) and

               A213: v in S and

               A214: (F . v) = y by A205, FUNCT_1:def 6;

              S c= ( conv ( @ S)) by RLAFFIN1: 2;

              then v in ( conv ( @ S)) by A213;

              hence thesis by A9, A208, A209, A212, A214;

            end;

            then ( card Aa) <= ( card B) by NAT_1: 43;

            then

             A215: Aa = B by A5, A210, A211, CARD_2: 102, XXREAL_0: 1;

            

             A216: the topology of ( BCS (k,CAa)) c= the topology of ( BCS (k,CA)) by A14, SIMPLEX0:def 13;

            

             A217: ( card S) = m by A95, A83, A71, A45, SIMPLEX0:def 18;

            then S is non empty by A30;

            then

             A218: (( center_of_mass V) . S) in ( Int ( @ S)) by RLAFFIN2: 20;

            ( Int ( @ S)) c= ( conv ( @ S)) by RLAFFIN2: 5;

            then (( center_of_mass V) . S) in ( conv ( @ S)) by A218;

            then

            consider w be Subset of ( BCS (k,CAa)) such that

             A219: w is simplex-like and

             A220: (( center_of_mass V) . S) in ( conv ( @ w)) by A65, A208, A215, Def3;

            w in the topology of ( BCS (k,CAa)) by A219;

            then w in the topology of ( BCS (k,CA)) by A216;

            then

            reconsider W = w as Simplex of ( BCS (k,CA)) by PRE_TOPC:def 2;

            ( Int ( @ S)) meets ( conv ( @ W)) by A218, A220, XBOOLE_0: 3;

            then

             A221: S c= w by Th26;

            then

            reconsider s = S as Subset of ( BCS (k,CAa)) by XBOOLE_1: 1;

            reconsider s as Simplex of ( BCS (k,CAa)) by A219, A221, MATROID0: 1;

            

             A222: (FA .: s) = Aa by A205, RELAT_1: 129, SIMPLEX0: 17;

            s is Simplex of (m - 1), ( BCS (k,CAa)) by A167, A217, SIMPLEX0: 48;

            hence thesis by A204, A222;

          end;

          

           A223: ( degree CAa) = (m - 1) by A5, A167, SIMPLEX0: 26;

          XXa c= XXA

          proof

            A <> Aa by A3, A5;

            then

             A224: Aa c< A by A12;

            let x be object;

            assume x in XXa;

            then

            consider S be Simplex of (m - 1), ( BCS (k,CAa)) such that

             A225: x = S and

             A226: (FA .: S) = Aa;

            (m - 1) <= ( degree ( BCS (k,CAa))) by A7, A223, Th32;

            then

            reconsider S1 = x as Simplex of (m - 1), ( BCS (k,CA)) by A14, A225, SIMPLEX0: 49;

            

             A227: (FA .: S) = (F .: S) by RELAT_1: 129, SIMPLEX0: 17;

            ( conv ( @ S)) c= ( conv Aa) by A65, Th5;

            then ( conv ( @ S1)) misses ( Int A) by A224, A225, RLAFFIN2: 7, XBOOLE_1: 63;

            hence thesis by A225, A226, A227;

          end;

          then

           A228: XXa = XXA by A203;

          for x be object st x in DX holds ( card ( Im (RDX,x))) = 2

          proof

            let x be object;

            assume

             A229: x in DX;

            then ex y be object st [x, y] in R by XTUPLE_0:def 12;

            then

             A230: x in Xm1 by A46;

            then

            consider S be Simplex of (m - 1), ( BCS (k,CA)) such that

             A231: x = S and

             A232: Aa = (F .: S);

            set XX = { S1 where S1 be Simplex of m, ( BCS (k,CA)) : S c= S1 };

             not x in XXA by A229, XBOOLE_0:def 5;

            then ( conv ( @ S)) meets ( Int A) by A231, A232;

            then

             A233: ( card XX) = 2 by A3, Th45;

            

             A234: (RDX .: {S}) c= XX

            proof

              let w be object;

              reconsider ww = w as set by TARSKI: 1;

              assume w in (RDX .: {S});

              then

              consider s be object such that

               A235: [s, w] in RDX and

               A236: s in {S} by RELAT_1:def 13;

              

               A237: [s, w] in R by A235, RELAT_1:def 11;

              then w in Xm by A46;

              then

               A238: ex W be Simplex of m, ( BCS (k,CA)) st w = W;

              s = S by A236, TARSKI:def 1;

              then P[S, ww] by A46, A237;

              then S c= ww;

              hence thesis by A238;

            end;

            XX c= (RDX .: {S})

            proof

              let w be object;

              assume w in XX;

              then

              consider W be Simplex of m, ( BCS (k,CA)) such that

               A239: w = W and

               A240: S c= W;

              W in Xm;

              then [S, W] in R by A46, A230, A231, A240;

              then

               A241: [S, W] in RDX by A229, A231, RELAT_1:def 11;

              S in {S} by TARSKI:def 1;

              hence thesis by A239, A241, RELAT_1:def 13;

            end;

            then XX = (RDX .: {S}) by A234;

            hence thesis by A231, A233, RELAT_1:def 16;

          end;

          

          then ( card RDX) = (( card (RDX | (( dom RDX) \ DX))) +` (2 *` ( card DX))) by Th1

          .= ( 0 +` (2 *` ( card DX))) by A67

          .= (2 *` ( card DX)) by CARD_2: 18;

          

          then

           A242: ( card R) = ((2 *` ( card DX)) +` (1 *` ( card XXA))) by A84, Th1

          .= ((2 *` ( card DX)) +` ((2 * n) + 1)) by A82, A228, CARD_2: 21

          .= ((( card 2) *` ( card ( card DX))) +` ((2 * n) + 1))

          .= (( card (2 * ( card DX))) +` ((2 * n) + 1)) by CARD_2: 39

          .= (( card (2 * ( card DX))) +` ( card ((2 * n) + 1)))

          .= ( card ((2 * ( card DX)) + ((2 * n) + 1))) by CARD_2: 38

          .= ((2 * ( card DX)) + ((2 * n) + 1));

          then ( card XX) = ((2 * ((( card DX) + n) - ( card YA))) + 1) by A47, A201;

          then (2 * ((( card DX) + n) - ( card YA))) >= ( - 1) by INT_1: 7;

          then ((( card DX) + n) - ( card YA)) >= (( - 1) / 2) by XREAL_1: 79;

          then ((( card DX) + n) - ( card YA)) > ( - 1) by XXREAL_0: 2;

          then ((( card DX) + n) - ( card YA)) >= 0 by INT_1: 8;

          then

          reconsider cnc = ((( card DX) + n) - ( card YA)) as Element of NAT by INT_1: 3;

          take cnc;

          thus thesis by A47, A201, A242;

        end;

      end;

      

       A243: P[ 0 qua Nat]

      proof

        let A be finite affinely-independent Subset of V such that

         A244: ( card A) = 0 ;

        

         A245: A = {} by A244;

        set C = ( Complex_of {A});

        

         A246: |.C.| c= ( [#] V) & ( [#] C) = ( [#] V);

        let F be Function of ( Vertices ( BCS (k,C))), A such that for v be Vertex of ( BCS (k,C)) holds for B be Subset of V st B c= A & v in ( conv B) holds (F . v) in B;

        set X = { S where S be Simplex of (( card A) - 1), ( BCS (k,C)) : (F .: S) = A };

        take 0 ;

        

         A247: k = 0 or k > 0 ;

        

         A248: (Z - 1) = ( - 1) by XXREAL_3: 4;

        then ( degree C) = ( - 1) by A244, SIMPLEX0: 26;

        then

         A249: C = ( BCS (k,C)) by A246, A247, Th16, Th22;

        

         A250: the topology of C = ( bool A) by SIMPLEX0: 4;

        

         A251: X c= {A}

        proof

          let x be object such that

           A252: x in X;

          consider S be Simplex of (( card A) - 1), ( BCS (k,C)) such that

           A253: S = x and (F .: S) = A by A252;

          S in the topology of C by A249, PRE_TOPC:def 2;

          then S is empty by A245, A250;

          hence thesis by A245, A253, TARSKI:def 1;

        end;

        A in ( bool A) by ZFMISC_1:def 1;

        then

        reconsider A1 = A as Simplex of C by A250, PRE_TOPC:def 2;

        

         A254: (F .: A1) = A by A245;

        A1 is Simplex of ( - 1), C by A244, A248, SIMPLEX0: 48;

        then A in X by A249, A254;

        then X = {A} by A251, ZFMISC_1: 33;

        hence thesis by CARD_1: 30;

      end;

      for k holds P[k] from NAT_1:sch 2( A243, A1);

      hence thesis;

    end;

    theorem :: SIMPLEX1:47

    for F st for v, B st B c= Aff & v in ( conv B) holds (F . v) in B holds ex S be Simplex of (( card Aff) - 1), ( BCS (k,( Complex_of {Aff}))) st (F .: S) = Aff

    proof

      let F be Function of ( Vertices ( BCS (k,( Complex_of {Aff})))), Aff;

      set XX = { S where S be Simplex of (( card Aff) - 1), ( BCS (k,( Complex_of {Aff}))) : (F .: S) = Aff };

      assume for v be Vertex of ( BCS (k,( Complex_of {Aff}))) holds for B st B c= Aff & v in ( conv B) holds (F . v) in B;

      then ex n st ( card XX) = ((2 * n) + 1) by Th46;

      then XX is non empty;

      then

      consider x be object such that

       A1: x in XX;

      ex S be Simplex of (( card Aff) - 1), ( BCS (k,( Complex_of {Aff}))) st x = S & (F .: S) = Aff by A1;

      hence thesis;

    end;