simplex0.miz



    begin

    reserve x,y,X,Y,Z for set,

D for non empty set,

n,k for Nat,

i,i1,i2 for Integer;

    notation

      let X;

      antonym X is with_empty_element for X is with_non-empty_elements;

    end

    registration

      cluster empty -> subset-closed for set;

      coherence ;

      cluster with_empty_element -> non empty for set;

      coherence ;

      cluster non empty subset-closed -> with_empty_element for set;

      coherence

      proof

        let X;

        assume

         A1: X is non empty subset-closed;

        then

        consider x be object such that

         A2: x in X;

        reconsider x as set by TARSKI: 1;

         {} c= x;

        then {} in X by A1, A2;

        hence thesis;

      end;

    end

    registration

      let X;

      cluster ( Sub_of_Fin X) -> finite-membered;

      coherence by COHSP_1:def 3;

    end

    registration

      let X be subset-closed set;

      cluster ( Sub_of_Fin X) -> subset-closed;

      coherence ;

    end

    theorem :: SIMPLEX0:1

    Y is subset-closed iff for X st X in Y holds ( bool X) c= Y

    proof

      thus Y is subset-closed implies for X st X in Y holds ( bool X) c= Y;

      assume

       A1: for X st X in Y holds ( bool X) c= Y;

      let x, y;

      assume that

       A2: x in Y and

       A3: y c= x;

      

       A4: y in ( bool x) by A3;

      ( bool x) c= Y by A1, A2;

      hence thesis by A4;

    end;

    registration

      let A,B be subset-closed set;

      cluster (A \/ B) -> subset-closed;

      coherence

      proof

        let x, y;

        assume that

         A1: x in (A \/ B) and

         A2: y c= x;

        x in A or x in B by A1, XBOOLE_0:def 3;

        then y in A or y in B by A2, CLASSES1:def 1;

        hence y in (A \/ B) by XBOOLE_0:def 3;

      end;

      cluster (A /\ B) -> subset-closed;

      coherence

      proof

        let x, y;

        assume that

         A3: x in (A /\ B) and

         A4: y c= x;

        x in B by A3, XBOOLE_0:def 4;

        then

         A5: y in B by A4, CLASSES1:def 1;

        x in A by A3, XBOOLE_0:def 4;

        then y in A by A4, CLASSES1:def 1;

        hence y in (A /\ B) by A5, XBOOLE_0:def 4;

      end;

    end

    

     Lm1: for X holds ex F be subset-closed set st F = ( union { ( bool x) where x be Element of X : x in X }) & X c= F & for Y st X c= Y & Y is subset-closed holds F c= Y

    proof

      let X;

      set B = { ( bool x) where x be Element of X : x in X };

      now

        let a,b be set such that

         A1: a in ( union B) and

         A2: b c= a;

        consider y such that

         A3: a in y and

         A4: y in B by A1, TARSKI:def 4;

        consider x be Element of X such that

         A5: y = ( bool x) and x in X by A4;

        b c= x by A2, A3, A5, XBOOLE_1: 1;

        hence b in ( union B) by A4, A5, TARSKI:def 4;

      end;

      then

      reconsider U = ( union B) as subset-closed set by CLASSES1:def 1;

      take U;

      thus U = ( union B);

      thus X c= U

      proof

        let x be object such that

         A6: x in X;

        reconsider xx = x as set by TARSKI: 1;

        xx c= xx & ( bool xx) in B by A6;

        hence thesis by TARSKI:def 4;

      end;

      let Y such that

       A7: X c= Y & Y is subset-closed;

      let x be object;

      assume x in U;

      then

      consider y such that

       A8: x in y and

       A9: y in B by TARSKI:def 4;

      ex x be Element of X st y = ( bool x) & x in X by A9;

      hence x in Y by A7, A8;

    end;

    definition

      let X;

      :: SIMPLEX0:def1

      func subset-closed_closure_of X -> subset-closed set means

      : Def1: X c= it & for Y st X c= Y & Y is subset-closed holds it c= Y;

      existence

      proof

        ex F be subset-closed set st F = ( union { ( bool x) where x be Element of X : x in X }) & X c= F & for Y st X c= Y & Y is subset-closed holds F c= Y by Lm1;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: SIMPLEX0:2

    

     Th2: x in ( subset-closed_closure_of X) iff ex y st x c= y & y in X

    proof

      set B = { ( bool x1) where x1 be Element of X : x1 in X };

      consider F be subset-closed set such that

       A1: F = ( union B) and

       A2: X c= F & for Y st X c= Y & Y is subset-closed holds F c= Y by Lm1;

      

       A3: F = ( subset-closed_closure_of X) by A2, Def1;

      hereby

        assume x in ( subset-closed_closure_of X);

        then

        consider y such that

         A4: x in y and

         A5: y in B by A1, A3, TARSKI:def 4;

        consider x1 be Element of X such that

         A6: ( bool x1) = y & x1 in X by A5;

        reconsider y = x1 as set;

        take y;

        thus x c= y & y in X by A4, A6;

      end;

      given y such that

       A7: x c= y and

       A8: y in X;

      ( bool y) in B by A8;

      hence thesis by A1, A3, A7, TARSKI:def 4;

    end;

    definition

      let X;

      let F be Subset-Family of X;

      :: original: subset-closed_closure_of

      redefine

      func subset-closed_closure_of F -> subset-closed Subset-Family of X ;

      coherence

      proof

        set FIC = ( subset-closed_closure_of F);

        FIC c= ( bool X)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in FIC;

          then ex y st xx c= y & y in F by Th2;

          then xx c= X by XBOOLE_1: 1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      cluster ( subset-closed_closure_of {} ) -> empty;

      coherence

      proof

        assume ( subset-closed_closure_of {} ) is non empty;

        then

        consider x be object such that

         A1: x in ( subset-closed_closure_of {} );

        reconsider x as set by TARSKI: 1;

        ex y st x c= y & y in {} by A1, Th2;

        hence thesis;

      end;

      let X be non empty set;

      cluster ( subset-closed_closure_of X) -> non empty;

      coherence

      proof

        ex x be object st x in X by XBOOLE_0:def 1;

        hence thesis by Th2;

      end;

    end

    registration

      let X be with_non-empty_element set;

      cluster ( subset-closed_closure_of X) -> with_non-empty_element;

      coherence

      proof

        consider b be non empty set such that

         A1: b in X by SETFAM_1:def 10;

        b in ( subset-closed_closure_of X) by A1, Th2;

        hence thesis;

      end;

    end

    registration

      let X be finite-membered set;

      cluster ( subset-closed_closure_of X) -> finite-membered;

      coherence

      proof

        let x be set;

        assume x in ( subset-closed_closure_of X);

        then

        consider y such that

         A1: x c= y and

         A2: y in X by Th2;

        y is finite by A2;

        hence thesis by A1;

      end;

    end

    theorem :: SIMPLEX0:3

    

     Th3: X c= Y & Y is subset-closed implies ( subset-closed_closure_of X) c= Y

    proof

      assume

       A1: X c= Y & Y is subset-closed;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in ( subset-closed_closure_of X);

      then ex y st xx c= y & y in X by Th2;

      hence thesis by A1;

    end;

    theorem :: SIMPLEX0:4

    

     Th4: ( subset-closed_closure_of {X}) = ( bool X)

    proof

      set f = ( subset-closed_closure_of {X});

      

       A1: X in {X} by TARSKI:def 1;

      hereby

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in f;

        then

        consider y such that

         A2: xx c= y and

         A3: y in {X} by Th2;

        y = X by A3, TARSKI:def 1;

        hence x in ( bool X) by A2;

      end;

      let x be object;

      assume x in ( bool X);

      hence thesis by A1, Th2;

    end;

    theorem :: SIMPLEX0:5

    ( subset-closed_closure_of (X \/ Y)) = (( subset-closed_closure_of X) \/ ( subset-closed_closure_of Y))

    proof

      set fxy = ( subset-closed_closure_of (X \/ Y));

      set fx = ( subset-closed_closure_of X);

      set fy = ( subset-closed_closure_of Y);

      hereby

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in fxy;

        then

        consider y such that

         A1: xx c= y and

         A2: y in (X \/ Y) by Th2;

        y in X or y in Y by A2, XBOOLE_0:def 3;

        then x in fx or x in fy by A1, Th2;

        hence x in (fx \/ fy) by XBOOLE_0:def 3;

      end;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume

       A3: x in (fx \/ fy);

      per cases by A3, XBOOLE_0:def 3;

        suppose x in fx;

        then

        consider y such that

         A4: xx c= y and

         A5: y in X by Th2;

        y in (X \/ Y) by A5, XBOOLE_0:def 3;

        hence thesis by A4, Th2;

      end;

        suppose x in fy;

        then

        consider y such that

         A6: xx c= y and

         A7: y in Y by Th2;

        y in (X \/ Y) by A7, XBOOLE_0:def 3;

        hence thesis by A6, Th2;

      end;

    end;

    theorem :: SIMPLEX0:6

    

     Th6: X is_finer_than Y iff ( subset-closed_closure_of X) c= ( subset-closed_closure_of Y)

    proof

      set fx = ( subset-closed_closure_of X);

      set fy = ( subset-closed_closure_of Y);

      hereby

        assume

         A1: X is_finer_than Y;

        thus fx c= fy

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in fx;

          then

          consider y such that

           A2: xx c= y and

           A3: y in X by Th2;

          consider c be set such that

           A4: c in Y and

           A5: y c= c by A1, A3;

          xx c= c by A2, A5;

          hence thesis by A4, Th2;

        end;

      end;

      assume

       A6: fx c= fy;

      let x;

      assume x in X;

      then x in fx by Th2;

      then ex y st x c= y & y in Y by A6, Th2;

      hence thesis;

    end;

    theorem :: SIMPLEX0:7

    

     Th7: X is subset-closed implies ( subset-closed_closure_of X) = X by Def1;

    theorem :: SIMPLEX0:8

    ( subset-closed_closure_of X) c= X implies X is subset-closed

    proof

      set f = ( subset-closed_closure_of X);

      assume

       A1: f c= X;

      let x, y;

      assume x in X & y c= x;

      then y in f by Th2;

      hence y in X by A1;

    end;

    definition

      let Y, X;

      let n be set;

      :: SIMPLEX0:def2

      func the_subsets_with_limited_card (n,X,Y) -> Subset-Family of Y means

      : Def2: for A be Subset of Y holds A in it iff A in X & ( card A) c= n;

      existence

      proof

        set SS = { A where A be Subset of Y : A in X & ( card A) c= n };

        SS c= ( bool Y)

        proof

          let x be object;

          assume x in SS;

          then ex A be Subset of Y st x = A & A in X & ( card A) c= n;

          hence thesis;

        end;

        then

        reconsider SS as Subset-Family of Y;

        take SS;

        let A be Subset of Y;

        hereby

          assume A in SS;

          then ex B be Subset of Y st B = A & B in X & ( card B) c= n;

          hence A in X & ( card A) c= n;

        end;

        assume A in X & ( card A) c= n;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be Subset-Family of Y;

        assume that

         A1: for A be Subset of Y holds A in S1 iff A in X & ( card A) c= n and

         A2: for A be Subset of Y holds A in S2 iff A in X & ( card A) c= n;

        thus S1 c= S2

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume

           A3: x in S1;

          then x in X & ( card xx) c= n by A1;

          hence thesis by A2, A3;

        end;

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A4: x in S2;

        then x in X & ( card xx) c= n by A2;

        hence thesis by A1, A4;

      end;

    end

    registration

      let D;

      cluster finite with_non-empty_element subset-closed finite-membered for Subset-Family of D;

      existence

      proof

        consider x be object such that

         A1: x in D by XBOOLE_0:def 1;

         {x} c= D by A1, ZFMISC_1: 31;

        then

        reconsider XX = ( bool {x}) as Subset-Family of D by ZFMISC_1: 67;

        take XX;

         {x} in ( bool {x}) by ZFMISC_1:def 1;

        hence thesis;

      end;

    end

    registration

      let Y, X;

      let n be finite Cardinal;

      cluster ( the_subsets_with_limited_card (n,X,Y)) -> finite-membered;

      coherence

      proof

        let A be set;

        assume A in ( the_subsets_with_limited_card (n,X,Y));

        then ( card A) c= ( card n) by Def2;

        hence thesis;

      end;

    end

    registration

      let Y;

      let X be subset-closed set;

      let n be Cardinal;

      cluster ( the_subsets_with_limited_card (n,X,Y)) -> subset-closed;

      coherence

      proof

        let x, y;

        assume that

         A1: x in ( the_subsets_with_limited_card (n,X,Y)) and

         A2: y c= x;

        x in X by A1, Def2;

        then

         A3: y in X by A2, CLASSES1:def 1;

        ( card x) c= ( card n) & ( card y) c= ( card x) by A1, A2, Def2, CARD_1: 11;

        then

         A4: ( card y) c= ( card n);

        y c= Y by A1, A2, XBOOLE_1: 1;

        hence thesis by A3, A4, Def2;

      end;

    end

    registration

      let Y;

      let X be with_empty_element set;

      let n be Cardinal;

      cluster ( the_subsets_with_limited_card (n,X,Y)) -> with_empty_element;

      coherence

      proof

        

         A1: {} c= Y;

        ( card {} ) c= ( card n) & {} in X by SETFAM_1:def 8;

        then {} in ( the_subsets_with_limited_card (n,X,Y)) by A1, Def2;

        hence thesis;

      end;

    end

    registration

      let D;

      let X be with_non-empty_element subset-closed Subset-Family of D;

      let n be non empty Cardinal;

      cluster ( the_subsets_with_limited_card (n,X,D)) -> with_non-empty_element;

      coherence

      proof

        consider x be non empty set such that

         A1: x in X by SETFAM_1:def 10;

        consider y be object such that

         A2: y in x by XBOOLE_0:def 1;

         {} c= ( card n);

        then {} in ( card n) by CARD_1: 3;

        then 1 c= ( card n) by CARD_2: 68;

        then

         A3: ( card {y}) c= ( card n) by CARD_1: 30;

         {y} c= x by A2, ZFMISC_1: 31;

        then {y} in X by A1, CLASSES1:def 1;

        then {y} in ( the_subsets_with_limited_card (n,X,D)) by A3, Def2;

        hence thesis;

      end;

    end

    notation

      let X;

      let Y be Subset-Family of X;

      let n be set;

      synonym the_subsets_with_limited_card (n,Y) for the_subsets_with_limited_card (n,Y,X);

    end

    theorem :: SIMPLEX0:9

    

     Th9: X is non empty finite c=-linear implies ( union X) in X

    proof

      assume X is non empty finite c=-linear;

      then

      consider U be set such that

       A1: U in X and

       A2: for x st x in X holds x c= U by FINSET_1: 12;

      

       A3: ( union X) c= U

      proof

        let x be object;

        assume x in ( union X);

        then

        consider y such that

         A4: x in y and

         A5: y in X by TARSKI:def 4;

        y c= U by A2, A5;

        hence thesis by A4;

      end;

      U c= ( union X) by A1, ZFMISC_1: 74;

      hence thesis by A1, A3, XBOOLE_0:def 10;

    end;

    theorem :: SIMPLEX0:10

    

     Th10: for X be finite c=-linear set st X is with_non-empty_elements holds ( card X) c= ( card ( union X))

    proof

      let X be finite c=-linear set;

      defpred P[ Nat] means for X be finite c=-linear set st X is with_non-empty_elements & ( card ( union X)) = $1 holds ( card X) c= ( card ( union X));

      defpred Q[ Nat] means for n be Nat st n <= $1 holds P[n];

      assume

       A1: X is with_non-empty_elements;

      

       A2: for m be Nat st Q[m] holds Q[(m + 1)]

      proof

        let m be Nat such that

         A3: Q[m];

        let n be Nat;

        assume

         A4: n <= (m + 1);

        let X be finite c=-linear set such that

         A5: X is with_non-empty_elements and

         A6: ( card ( union X)) = n;

        reconsider u = ( union X) as finite set by A6;

        reconsider Xu = (X \ {u}) as finite c=-linear set;

        per cases by A4, NAT_1: 8;

          suppose n <= m;

          hence thesis by A3, A5, A6;

        end;

          suppose

           A7: n = (m + 1);

          then X is non empty by A6, ZFMISC_1: 2;

          then

           A8: X = (Xu \/ {u}) by Th9, ZFMISC_1: 116;

          

          then u = (( union Xu) \/ ( union {u})) by ZFMISC_1: 78

          .= (( union Xu) \/ u) by ZFMISC_1: 25;

          then

           A9: ( union Xu) c= u by XBOOLE_1: 11;

          then

          reconsider uXu = ( union Xu) as finite set;

          uXu <> u

          proof

            assume

             A10: uXu = u;

            then Xu is non empty by A6, A7, ZFMISC_1: 2;

            then u in Xu by A10, Th9;

            hence thesis by ZFMISC_1: 56;

          end;

          then

           A11: uXu c< u by A9;

          then ( card uXu) < (m + 1) by A6, A7, CARD_2: 48;

          then ( card uXu) <= m by NAT_1: 13;

          then ( Segm ( card Xu)) c= ( Segm ( card uXu)) by A3, A5;

          then ( card Xu) <= ( card uXu) by NAT_1: 39;

          then ( card Xu) < ( card u) by A11, CARD_2: 48, XXREAL_0: 2;

          then

           A12: (1 + ( card Xu)) <= ( card u) by NAT_1: 13;

           not u in Xu by ZFMISC_1: 56;

          then

           A13: (1 + ( card Xu)) = ( card X) by A8, CARD_2: 41;

          ( Segm (1 + ( card Xu))) c= ( Segm ( card u)) by A12, NAT_1: 39;

          hence thesis by A13;

        end;

      end;

      

       A14: Q[ 0 ]

      proof

        let n be Nat;

        assume

         A15: n <= 0 ;

        let X be finite c=-linear set such that

         A16: X is with_non-empty_elements & ( card ( union X)) = n;

        X is empty by A15, A16;

        hence ( card X) c= ( card ( union X));

      end;

      for n be Nat holds Q[n] from NAT_1:sch 2( A14, A2);

      hence thesis by A1;

    end;

    theorem :: SIMPLEX0:11

    X is c=-linear implies (X \/ {(( union X) \/ x)}) is c=-linear

    proof

      assume that

       A1: X is c=-linear;

      set U = ( union X);

      set Ux = (U \/ x);

      

       A2: U c= Ux by XBOOLE_1: 7;

      let x1,x2 be set such that

       A3: x1 in (X \/ {Ux}) & x2 in (X \/ {Ux});

      per cases by A3, XBOOLE_0:def 3;

        suppose x1 in X & x2 in X;

        hence thesis by A1;

      end;

        suppose

         A4: x1 in {Ux} & x2 in {Ux};

        then x1 = Ux by TARSKI:def 1;

        hence thesis by A4, TARSKI:def 1;

      end;

        suppose x1 in X & x2 in {Ux};

        then x1 c= U & x2 = Ux by TARSKI:def 1, ZFMISC_1: 74;

        then x1 c= x2 by A2;

        hence thesis;

      end;

        suppose x2 in X & x1 in {Ux};

        then x2 c= U & x1 = Ux by TARSKI:def 1, ZFMISC_1: 74;

        then x2 c= x1 by A2;

        hence thesis;

      end;

    end;

    theorem :: SIMPLEX0:12

    

     Th12: for X be non empty set holds ex Y be Subset-Family of X st Y is with_non-empty_elements c=-linear & X in Y & ( card X) = ( card Y) & for Z st Z in Y & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in Y

    proof

      let X be non empty set;

      consider R be Relation such that

       A1: R well_orders X by WELLORD2: 17;

      set RX = (R |_2 X);

      deffunc F( object) = (X \ (RX -Seg $1));

      

       A2: for x be object st x in X holds F(x) in ( bool X);

      consider f be Function of X, ( bool X) such that

       A3: for x be object st x in X holds (f . x) = F(x) from FUNCT_2:sch 2( A2);

      take Y = ( rng f);

      

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

      thus Y is with_non-empty_elements

      proof

        assume Y is with_empty_element;

        then {} in Y;

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: (f . x) = {} by FUNCT_1:def 3;

         {} = F(x) by A3, A5, A6;

        then X c= (RX -Seg x) by XBOOLE_1: 37;

        hence thesis by A4, A5, WELLORD1: 1;

      end;

      thus Y is c=-linear

      proof

        let x, y;

        assume that

         A7: x in Y and

         A8: y in Y;

        consider a be object such that

         A9: a in ( dom f) & (f . a) = x by A7, FUNCT_1:def 3;

        consider b be object such that

         A10: b in ( dom f) & (f . b) = y by A8, FUNCT_1:def 3;

        ((RX -Seg a),(RX -Seg b)) are_c=-comparable by A1, WELLORD1: 26, WELLORD2: 16;

        then (RX -Seg a) c= (RX -Seg b) or (RX -Seg b) c= (RX -Seg a);

        then F(b) c= F(a) or F(a) c= F(b) by XBOOLE_1: 34;

        then

         A11: ( F(a), F(b)) are_c=-comparable ;

        x = F(a) by A3, A9;

        hence thesis by A3, A10, A11;

      end;

      

       A12: ( field RX) = X by A1, WELLORD2: 16;

      then

      consider x be object such that

       A13: x in X and

       A14: for y be object st y in X holds [x, y] in RX by A1, WELLORD1: 7, WELLORD2: 16;

      

       A15: RX is well-ordering by A1, WELLORD2: 16;

      then

       A16: RX is well_founded by WELLORD1:def 4;

      RX is antisymmetric by A15, WELLORD1:def 4;

      then

       A17: RX is_antisymmetric_in X by A12, RELAT_2:def 12;

      

       A18: (RX -Seg x) = {}

      proof

        assume (RX -Seg x) <> {} ;

        then

        consider y be object such that

         A19: y in (RX -Seg x) by XBOOLE_0:def 1;

        

         A20: y <> x by A19, WELLORD1: 1;

        

         A21: [y, x] in RX by A19, WELLORD1: 1;

        then

         A22: x in X by A12, RELAT_1: 15;

        

         A23: y in X by A12, A21, RELAT_1: 15;

        then [x, y] in RX by A14;

        hence thesis by A17, A20, A21, A22, A23, RELAT_2:def 4;

      end;

      (f . x) = F(x) by A3, A13;

      hence X in Y by A4, A13, A18, FUNCT_1:def 3;

      now

        let x1,x2 be object;

        reconsider R1 = (RX -Seg x1), R2 = (RX -Seg x2) as Subset of X by A12, WELLORD1: 9;

        assume that

         A24: x1 in X & x2 in X and

         A25: (f . x1) = (f . x2);

        (R1 ` ) = (f . x1) & (f . x2) = (R2 ` ) by A3, A24;

        then R1 = R2 by A25, SUBSET_1: 42;

        then [x1, x2] in RX & [x2, x1] in RX by A12, A15, A24, WELLORD1: 29;

        hence x1 = x2 by A17, A24, RELAT_2:def 4;

      end;

      then f is one-to-one by FUNCT_2: 19;

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

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

      let Z;

      assume that

       A26: Z in Y and

       A27: ( card Z) <> 1;

      consider x be object such that

       A28: x in ( dom f) and

       A29: (f . x) = Z by A26, FUNCT_1:def 3;

      

       A30: {x} c= X by A28, ZFMISC_1: 31;

      reconsider x as set by TARSKI: 1;

      take x;

      

       A31: not x in (RX -Seg x) by WELLORD1: 1;

      

       A32: Z = (X \ (RX -Seg x)) by A3, A28, A29;

      hence x in Z by A28, A31, XBOOLE_0:def 5;

      (RX -Seg x) c= X by A12, WELLORD1: 9;

      then

      reconsider Rxx = ((RX -Seg x) \/ {x}) as Subset of X by A30, XBOOLE_1: 8;

      (X \ Rxx) <> {}

      proof

        assume (X \ Rxx) = {} ;

        then X c= Rxx by XBOOLE_1: 37;

        

        then Z = (Rxx \ (RX -Seg x)) by A32, XBOOLE_0:def 10

        .= ( {x} \ (RX -Seg x)) by XBOOLE_1: 40

        .= {x} by A31, ZFMISC_1: 59;

        hence contradiction by A27, CARD_1: 30;

      end;

      then

      consider a be object such that

       A33: a in (Rxx ` ) and

       A34: (RX -Seg a) misses (Rxx ` ) by A12, A16, WELLORD1:def 2;

      

       A35: not a in Rxx by A33, XBOOLE_0:def 5;

      x in {x} by TARSKI:def 1;

      then

       A36: x <> a by A35, XBOOLE_0:def 3;

      RX is connected by A15, WELLORD1:def 4;

      then RX is_connected_in X by A12, RELAT_2:def 14;

      then

       A37: [x, a] in RX or [a, x] in RX by A28, A33, A36, RELAT_2:def 6;

      

       A38: not a in (RX -Seg x) by A35, XBOOLE_0:def 3;

      then x in (RX -Seg a) by A36, A37, WELLORD1: 1;

      then

       A39: {x} c= (RX -Seg a) by ZFMISC_1: 31;

      (RX -Seg a) c= X by A12, WELLORD1: 9;

      then

       A40: (RX -Seg a) c= Rxx by A34, SUBSET_1: 24;

      (RX -Seg x) c= (RX -Seg a) by A12, A15, A28, A33, A37, A38, WELLORD1: 1, WELLORD1: 29;

      then Rxx c= (RX -Seg a) by A39, XBOOLE_1: 8;

      then Rxx = (RX -Seg a) by A40;

      

      then (f . a) = (X \ Rxx) by A3, A33

      .= ((X \ (RX -Seg x)) \ {x}) by XBOOLE_1: 41

      .= (Z \ {x}) by A3, A28, A29;

      hence thesis by A4, A33, FUNCT_1:def 3;

    end;

    theorem :: SIMPLEX0:13

    for Y be Subset-Family of X st Y is finite with_non-empty_elements c=-linear & X in Y holds ex Y1 be Subset-Family of X st Y c= Y1 & Y1 is with_non-empty_elements c=-linear & ( card X) = ( card Y1) & for Z st Z in Y1 & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in Y1

    proof

      let Y be Subset-Family of X such that

       A1: Y is finite with_non-empty_elements c=-linear and

       A2: X in Y;

      defpred P[ object, object] means ex A be set st A = $2 & $1 in A & $2 in Y & for y st y in Y & $1 in y holds A c= y;

      

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

      proof

        let x be object;

        set U = { A where A be Subset of X : x in A & A in Y };

        

         A4: U c= Y

        proof

          let y be object;

          assume y in U;

          then ex A be Subset of X st y = A & x in A & A in Y;

          hence thesis;

        end;

        then

        reconsider U as Subset-Family of X by XBOOLE_1: 1;

        assume x in X;

        then X in U by A2;

        then

        consider m be set such that

         A5: m in U and

         A6: for y st y in U holds m c= y by A1, A4, FINSET_1: 11;

        take m;

        consider A be Subset of X such that

         A7: m = A & x in A & A in Y by A5;

        take A;

        thus A = m by A7;

        thus x in A & m in Y by A7;

        let y;

        assume y in Y & x in y;

        then y in U;

        hence thesis by A6, A7;

      end;

      consider f be Function such that

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

      defpred Q[ object, object] means ex D1,D2 be set st D1 = $1 & D2 = $2 & (D2 in Y or D2 is empty) & D2 c< D1 & (for x st x in Y & x c< D1 holds x c= D2) & (for x st x in Y & D2 c= x & x c= D1 holds x = D1 or x = D2);

      

       A9: for x be object st x in Y holds ex y be object st y in ( bool X) & Q[x, y]

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A10: x in Y;

        set U = { A where A be Subset of X : A c< xx & A in Y };

        

         A11: U c= Y

        proof

          let y be object;

          assume y in U;

          then ex A be Subset of X st y = A & A c< xx & A in Y;

          hence thesis;

        end;

        then

        reconsider U as Subset-Family of X by XBOOLE_1: 1;

        take u = ( union U);

        thus u in ( bool X);

        

         A12: for y st y in Y & y c< xx holds y c= u

        proof

          let y;

          assume that

           A13: y in Y and

           A14: y c< xx;

          y in U by A13, A14;

          hence thesis by ZFMISC_1: 74;

        end;

        per cases ;

          suppose

           A15: U is empty;

          take xx, u;

          thus xx = x & u = u;

          thus (u in Y or u is empty) & u c< xx & for y st y in Y & y c< xx holds y c= u by A1, A10, A12, A15, XBOOLE_1: 61, ZFMISC_1: 2;

          let y;

          assume that

           A16: y in Y and

           A17: u c= y and

           A18: y c= xx;

          assume y <> xx;

          then y c< xx by A18;

          then y c= u by A12, A16;

          hence thesis by A17;

        end;

          suppose U is non empty;

          then u in U by A1, A11, Th9;

          then

           A19: ex A be Subset of X st A = u & A c< xx & A in Y;

          take xx, u;

          thus xx = x & u = u;

          thus (u in Y or u is empty) & u c< xx & for y st y in Y & y c< xx holds y c= u by A12, A19;

          let y;

          assume that

           A20: y in Y and

           A21: u c= y and

           A22: y c= xx;

          assume y <> xx;

          then y c< xx by A22;

          then y c= u by A12, A20;

          hence thesis by A21;

        end;

      end;

      consider g be Function of Y, ( bool X) such that

       A23: for x be object st x in Y holds Q[x, (g . x)] from FUNCT_2:sch 1( A9);

      defpred R[ object, object] means ex A be set, h be Function of (A \ (g . A)), ( bool (A \ (g . A))) st A = $1 & $2 = h & h is one-to-one & ( rng h) is with_non-empty_elements c=-linear & ( dom h) in ( rng h) & for Z st Z in ( rng h) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng h);

      

       A24: for x be object st x in Y holds ex y be object st R[x, y]

      proof

        let y be object;

        assume

         A25: y in Y;

        reconsider y as set by TARSKI: 1;

         Q[y, (g . y)] by A23, A25;

        then (g . y) c< y;

        then (y \ (g . y)) <> {} by XBOOLE_1: 105;

        then

        consider Z be Subset-Family of (y \ (g . y)) such that

         A26: Z is with_non-empty_elements c=-linear & (y \ (g . y)) in Z and

         A27: ( card (y \ (g . y))) = ( card Z) and

         A28: for z be set st z in Z & ( card z) <> 1 holds ex x st x in z & (z \ {x}) in Z by Th12;

        ((y \ (g . y)),Z) are_equipotent by A27, CARD_1: 5;

        then

        consider h be Function such that

         A29: h is one-to-one and

         A30: ( dom h) = (y \ (g . y)) & ( rng h) = Z by WELLORD2:def 4;

        reconsider h as Function of (y \ (g . y)), ( bool (y \ (g . y))) by A30, FUNCT_2: 2;

        take h;

        thus thesis by A26, A28, A29, A30;

      end;

      consider h be Function such that

       A31: ( dom h) = Y & for x be object st x in Y holds R[x, (h . x)] from CLASSES1:sch 1( A24);

      now

        let x be object;

        assume x in ( dom h);

        then R[x, (h . x)] by A31;

        hence (h . x) is Function;

      end;

      then

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

      deffunc Z( object) = ((g . (f . $1)) \/ ((h . (f . $1)) . $1));

      

       A32: for x st x in X holds x in ((f . x) \ (g . (f . x)))

      proof

        let x;

        assume x in X;

        then

         A33: P[x, (f . x)] by A8;

        then

         A34: (f . x) in Y;

        assume

         A35: not x in ((f . x) \ (g . (f . x)));

        x in (f . x) by A33;

        then

         A36: x in (g . (f . x)) by A35, XBOOLE_0:def 5;

        

         A37: Q[(f . x), (g . (f . x))] by A23, A34;

        then (g . (f . x)) in Y by A36;

        then

         A38: (f . x) c= (g . (f . x)) by A36, A33;

        (g . (f . x)) c< (f . x) by A37;

        hence thesis by A38, XBOOLE_0:def 8;

      end;

      

       A39: for x be object st x in X holds Z(x) in ( bool X)

      proof

        let x be object;

        set fx = (f . x);

        assume

         A40: x in X;

        then P[x, (f . x)] by A8;

        then

         A41: fx in Y;

        then R[fx, (h . fx)] by A31;

        then

        consider A be set, H be Function of (fx \ (g . fx)), ( bool (fx \ (g . fx))) such that

         A42: (h . fx) = H and H is one-to-one and ( rng H) is with_non-empty_elements c=-linear and ( dom H) in ( rng H) and for Z st Z in ( rng H) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H);

        

         A43: x in (fx \ (g . fx)) by A32, A40;

        ( dom H) = (fx \ (g . fx)) by FUNCT_2:def 1;

        then (H . x) in ( rng H) by A43, FUNCT_1:def 3;

        then (H . x) c= fx by XBOOLE_1: 1;

        then

         A44: (H . x) c= X by A41, XBOOLE_1: 1;

         Q[fx, (g . fx)] by A23, A41;

        then (g . fx) in Y or (g . fx) is empty;

        then Z(x) c= X by A42, A44, XBOOLE_1: 8;

        hence thesis;

      end;

      consider z be Function of X, ( bool X) such that

       A45: for x be object st x in X holds (z . x) = Z(x) from FUNCT_2:sch 2( A39);

      

       A46: ( dom z) = X by FUNCT_2:def 1;

      

       A47: Y c= ( rng z)

      proof

        let y be object;

        reconsider yy = y as set by TARSKI: 1;

        assume

         A48: y in Y;

        then R[y, (h . y)] by A31;

        then

        consider H be Function of (yy \ (g . y)), ( bool (yy \ (g . y))) such that

         A49: (h . y) = H and H is one-to-one and ( rng H) is with_non-empty_elements c=-linear and

         A50: ( dom H) in ( rng H) and for Z st Z in ( rng H) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H);

        consider x be object such that

         A51: x in ( dom H) and

         A52: (H . x) = ( dom H) by A50, FUNCT_1:def 3;

        

         A53: ( dom H) = (yy \ (g . yy)) by FUNCT_2:def 1;

        then

         A54: x in yy by A51;

        then

         A55: P[x, (f . x)] by A8, A48;

        then

         A56: x in (f . x);

         Q[y, (g . y)] by A23, A48;

        then (g . y) c< yy;

        then

         A57: (g . y) c= yy;

        

         A58: (f . x) c= yy by A48, A54, A55;

        

         A59: (f . x) in Y by A55;

        (f . x) = y

        proof

          assume (f . x) <> y;

          then

           A60: (f . x) c< yy by A58;

           Q[y, (g . y)] by A23, A48;

          then (f . x) c= (g . y) by A59, A60;

          hence contradiction by A51, A56, XBOOLE_0:def 5;

        end;

        

        then (z . x) = ((g . y) \/ (yy \ (g . y))) by A45, A48, A49, A52, A53, A54

        .= y by A57, XBOOLE_1: 45;

        hence thesis by A46, A48, A54, FUNCT_1:def 3;

      end;

      

       A61: for Z st Z in ( rng z) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng z)

      proof

        let Z;

        assume that

         A62: Z in ( rng z) and

         A63: ( card Z) <> 1;

        consider x be object such that

         A64: x in ( dom z) and

         A65: (z . x) = Z by A62, FUNCT_1:def 3;

        set fx = (f . x);

         P[x, fx] by A8, A64;

        then

         A66: fx in Y;

        then R[fx, (h . fx)] by A31;

        then

        consider H be Function of (fx \ (g . fx)), ( bool (fx \ (g . fx))) such that

         A67: (h . fx) = H and H is one-to-one and ( rng H) is with_non-empty_elements c=-linear and ( dom H) in ( rng H) and

         A68: for Z st Z in ( rng H) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H);

        

         A69: (z . x) = ((g . fx) \/ (H . x)) by A45, A64, A67;

        

         A70: ( dom H) = (fx \ (g . fx)) by FUNCT_2:def 1;

        x in (fx \ (g . fx)) by A32, A64;

        then

         A71: (H . x) in ( rng H) by A70, FUNCT_1:def 3;

        per cases ;

          suppose

           A72: ( card (H . x)) = 1;

          then

           A73: (g . fx) <> {} by A63, A65, A69;

           Q[fx, (g . fx)] by A23, A66;

          then

           A74: (g . fx) in Y by A73;

          consider a be object such that

           A75: (H . x) = {a} by A72, CARD_2: 42;

          reconsider a as set by TARSKI: 1;

          take a;

          

           A76: a in (H . x) by A75, TARSKI:def 1;

          then

           A77: not a in (g . fx) by A71, XBOOLE_0:def 5;

          thus a in Z by A65, A69, A76, XBOOLE_0:def 3;

          (Z \ {a}) = (((g . fx) \/ (H . x)) \ (H . x)) by A45, A64, A65, A67, A75

          .= ((g . fx) \ (H . x)) by XBOOLE_1: 40

          .= (g . fx) by A75, A77, ZFMISC_1: 57;

          hence thesis by A47, A74;

        end;

          suppose ( card (H . x)) <> 1;

          then

          consider a be set such that

           A78: a in (H . x) and

           A79: ((H . x) \ {a}) in ( rng H) by A68, A71;

          

           A80: not a in (g . fx) by A71, A78, XBOOLE_0:def 5;

          take a;

          thus a in Z by A65, A69, A78, XBOOLE_0:def 3;

          consider b be object such that

           A81: b in ( dom H) and

           A82: (H . b) = ((H . x) \ {a}) by A79, FUNCT_1:def 3;

          

           A83: b in fx by A70, A81;

          then

           A84: P[b, (f . b)] by A8, A66;

          then

           A85: b in (f . b);

          

           A86: (f . b) in Y by A84;

          

           A87: (f . b) c= fx by A66, A83, A84;

          fx = (f . b)

          proof

            assume fx <> (f . b);

            then

             A88: (f . b) c< fx by A87;

             Q[fx, (g . fx)] by A23, A66;

            then (f . b) c= (g . fx) by A86, A88;

            hence contradiction by A81, A85, XBOOLE_0:def 5;

          end;

          

          then (z . b) = ((g . fx) \/ ((H . x) \ {a})) by A45, A66, A67, A82, A83

          .= (((g . fx) \/ (H . x)) \ {a}) by A80, XBOOLE_1: 87, ZFMISC_1: 50

          .= (Z \ {a}) by A65, A45, A64, A67;

          hence thesis by A46, A66, A83, FUNCT_1:def 3;

        end;

      end;

      

       A89: ( rng z) is c=-linear

      proof

        let y1,y2 be set;

        assume that

         A90: y1 in ( rng z) and

         A91: y2 in ( rng z);

        consider x1 be object such that

         A92: x1 in ( dom z) and

         A93: (z . x1) = y1 by A90, FUNCT_1:def 3;

        consider x2 be object such that

         A94: x2 in ( dom z) and

         A95: (z . x2) = y2 by A91, FUNCT_1:def 3;

        set fx1 = (f . x1), fx2 = (f . x2);

        

         A96: x1 in (fx1 \ (g . fx1)) by A32, A92;

         P[x1, (f . x1)] by A8, A92;

        then

         A97: fx1 in Y;

        then R[fx1, (h . fx1)] by A31;

        then

        consider H1 be Function of (fx1 \ (g . fx1)), ( bool (fx1 \ (g . fx1))) such that

         A98: (h . fx1) = H1 and H1 is one-to-one and ( rng H1) is with_non-empty_elements c=-linear and ( dom H1) in ( rng H1) and for Z st Z in ( rng H1) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H1);

        

         A99: (z . x1) = ((g . fx1) \/ (H1 . x1)) by A45, A92, A98;

        ( dom H1) = (fx1 \ (g . fx1)) by FUNCT_2:def 1;

        then

         A100: (H1 . x1) in ( rng H1) by A96, FUNCT_1:def 3;

        

         A101: x2 in (fx2 \ (g . fx2)) by A32, A94;

         P[x2, fx2] by A8, A94;

        then

         A102: fx2 in Y;

        then R[fx2, (h . fx2)] by A31;

        then

        consider H2 be Function of (fx2 \ (g . fx2)), ( bool (fx2 \ (g . fx2))) such that

         A103: (h . fx2) = H2 and H2 is one-to-one and

         A104: ( rng H2) is with_non-empty_elements c=-linear and ( dom H2) in ( rng H2) and for Z st Z in ( rng H2) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H2);

        

         A105: (z . x2) = ((g . fx2) \/ (H2 . x2)) by A45, A94, A103;

        ( dom H2) = (fx2 \ (g . fx2)) by FUNCT_2:def 1;

        then

         A106: (H2 . x2) in ( rng H2) by A101, FUNCT_1:def 3;

        

         A107: (fx1,fx2) are_c=-comparable by A1, A97, A102;

        per cases by A107;

          suppose

           A108: fx1 = fx2;

          then ((H1 . x1),(H1 . x2)) are_c=-comparable by A98, A100, A103, A104, A106;

          then (H1 . x1) c= (H1 . x2) or (H1 . x2) c= (H1 . x1);

          then (z . x1) c= (z . x2) or (z . x2) c= (z . x1) by A98, A99, A103, A105, A108, XBOOLE_1: 9;

          hence thesis by A93, A95;

        end;

          suppose fx1 c= fx2 & fx1 <> fx2;

          then

           A109: fx1 c< fx2;

           Q[fx2, (g . fx2)] by A23, A102;

          then

           A110: fx1 c= (g . fx2) by A97, A109;

          (g . fx2) c= (z . x2) by A105, XBOOLE_1: 7;

          then

           A111: fx1 c= (z . x2) by A110;

           Q[fx1, (g . fx1)] by A23, A97;

          then (g . fx1) c< fx1;

          then (g . fx1) c= fx1;

          then

           A112: ((g . fx1) \/ (fx1 \ (g . fx1))) = fx1 by XBOOLE_1: 45;

          (z . x1) c= ((g . fx1) \/ (fx1 \ (g . fx1))) by A99, A100, XBOOLE_1: 9;

          then (z . x1) c= (z . x2) by A111, A112;

          hence thesis by A93, A95;

        end;

          suppose fx2 c= fx1 & fx1 <> fx2;

          then

           A113: fx2 c< fx1;

           Q[fx1, (g . fx1)] by A23, A97;

          then

           A114: fx2 c= (g . fx1) by A102, A113;

          (g . fx1) c= (z . x1) by A99, XBOOLE_1: 7;

          then

           A115: fx2 c= (z . x1) by A114;

           Q[fx2, (g . fx2)] by A23, A102;

          then (g . fx2) c< fx2;

          then (g . fx2) c= fx2;

          then

           A116: ((g . fx2) \/ (fx2 \ (g . fx2))) = fx2 by XBOOLE_1: 45;

          (z . x2) c= ((g . fx2) \/ (fx2 \ (g . fx2))) by A105, A106, XBOOLE_1: 9;

          then (z . x2) c= (z . x1) by A115, A116;

          hence thesis by A93, A95;

        end;

      end;

      

       A117: ( rng z) is with_non-empty_elements

      proof

        assume ( rng z) is non with_non-empty_elements;

        then {} in ( rng z);

        then

        consider x be object such that

         A118: x in ( dom z) and

         A119: (z . x) = {} by FUNCT_1:def 3;

        set fx = (f . x);

        

         A120: x in (fx \ (g . fx)) by A32, A118;

         P[x, fx] by A8, A118;

        then fx in Y;

        then R[fx, (h . fx)] by A31;

        then

        consider H be Function of (fx \ (g . fx)), ( bool (fx \ (g . fx))) such that

         A121: (h . fx) = H and H is one-to-one and

         A122: ( rng H) is with_non-empty_elements c=-linear and ( dom H) in ( rng H) and for Z st Z in ( rng H) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H);

        ( dom H) = (fx \ (g . fx)) by FUNCT_2:def 1;

        then

         A123: (H . x) in ( rng H) by A120, FUNCT_1:def 3;

        (z . x) = ((g . fx) \/ (H . x)) by A45, A118, A121;

        hence contradiction by A119, A122, A123;

      end;

      take ( rng z);

      for x1,x2 be object st x1 in ( dom z) & x2 in ( dom z) & (z . x1) = (z . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        set f1 = (f . x1), f2 = (f . x2);

        assume that

         A124: x1 in ( dom z) and

         A125: x2 in ( dom z) and

         A126: (z . x1) = (z . x2);

        

         A127: (z . x1) = Z(x1) & (z . x2) = Z(x2) by A45, A124, A125;

         P[x2, f2] by A8, A125;

        then

         A128: f2 in Y;

        then R[f2, (h . f2)] by A31;

        then

        consider H2 be Function of (f2 \ (g . f2)), ( bool (f2 \ (g . f2))) such that

         A129: (h . f2) = H2 and

         A130: H2 is one-to-one and

         A131: ( rng H2) is with_non-empty_elements c=-linear and ( dom H2) in ( rng H2) and for Z st Z in ( rng H2) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H2);

        ( dom H2) = (f2 \ (g . f2)) by FUNCT_2:def 1;

        then

         A132: x2 in ( dom H2) by A32, A125;

        then

         A133: (H2 . x2) in ( rng H2) by FUNCT_1:def 3;

        then

         A134: (g . f2) misses (H2 . x2) by XBOOLE_1: 63, XBOOLE_1: 79;

         P[x1, f1] by A8, A124;

        then

         A135: f1 in Y;

        then R[f1, (h . f1)] by A31;

        then

        consider H1 be Function of (f1 \ (g . f1)), ( bool (f1 \ (g . f1))) such that

         A136: (h . f1) = H1 and H1 is one-to-one and

         A137: ( rng H1) is with_non-empty_elements c=-linear and ( dom H1) in ( rng H1) and for Z st Z in ( rng H1) & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in ( rng H1);

        ( dom H1) = (f1 \ (g . f1)) by FUNCT_2:def 1;

        then

         A138: x1 in ( dom H1) by A32, A124;

        then

         A139: (H1 . x1) in ( rng H1) by FUNCT_1:def 3;

        then

         A140: (g . f1) misses (H1 . x1) by XBOOLE_1: 63, XBOOLE_1: 79;

        

         A141: (f1,f2) are_c=-comparable by A1, A128, A135;

        per cases by A141;

          suppose

           A142: f1 = f2;

          then (H1 . x1) = (H1 . x2) by A126, A127, A129, A134, A136, A140, XBOOLE_1: 71;

          hence thesis by A129, A130, A132, A136, A138, A142, FUNCT_1:def 4;

        end;

          suppose

           A143: f1 c= f2 & f1 <> f2;

           Q[f1, (g . f1)] by A23, A135;

          then (g . f1) c< f1;

          then (g . f1) c= f1;

          then ((g . f1) \/ (f1 \ (g . f1))) = f1 by XBOOLE_1: 45;

          then

           A144: Z(x2) c= f1 by A126, A127, A136, A139, XBOOLE_1: 9;

          

           A145: f1 c< f2 by A143;

           Q[f2, (g . f2)] by A23, A128;

          then f1 c= (g . f2) by A135, A145;

          then Z(x2) c= (g . f2) by A144;

          then (H2 . x2) c= (g . f2) by A129, XBOOLE_1: 11;

          hence thesis by A131, A133, XBOOLE_1: 67, XBOOLE_1: 79;

        end;

          suppose

           A146: f2 c= f1 & f1 <> f2;

           Q[f2, (g . f2)] by A23, A128;

          then (g . f2) c< f2;

          then (g . f2) c= f2;

          then ((g . f2) \/ (f2 \ (g . f2))) = f2 by XBOOLE_1: 45;

          then

           A147: Z(x1) c= f2 by A126, A127, A129, A133, XBOOLE_1: 9;

          

           A148: f2 c< f1 by A146;

           Q[f1, (g . f1)] by A23, A135;

          then f2 c= (g . f1) by A128, A148;

          then Z(x1) c= (g . f1) by A147;

          then (H1 . x1) c= (g . f1) by A136, XBOOLE_1: 11;

          hence thesis by A137, A139, XBOOLE_1: 67, XBOOLE_1: 79;

        end;

      end;

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

      then (X,( rng z)) are_equipotent by A46, WELLORD2:def 4;

      hence thesis by A47, A61, A89, A117, CARD_1: 5;

    end;

    begin

    definition

      mode SimplicialComplexStr is TopStruct;

    end

    reserve K for SimplicialComplexStr;

    notation

      let K;

      let A be Subset of K;

      synonym A is simplex-like for A is open;

    end

    notation

      let K;

      let S be Subset-Family of K;

      synonym S is simplex-like for S is open;

    end

    registration

      let K;

      cluster empty simplex-like for Subset-Family of K;

      existence

      proof

        take E = ( {} ( bool the carrier of K));

        thus thesis;

      end;

    end

    theorem :: SIMPLEX0:14

    

     Th14: for S be Subset-Family of K holds S is simplex-like iff S c= the topology of K

    proof

      let S be Subset-Family of K;

      hereby

        assume

         A1: S is simplex-like;

        thus S c= the topology of K

        proof

          let x be object;

          assume

           A2: x in S;

          then

          reconsider A = x as Subset of K;

          A is simplex-like by A1, A2;

          hence thesis;

        end;

      end;

      assume

       A3: S c= the topology of K;

      let A be Subset of K;

      assume A in S;

      hence thesis by A3;

    end;

    definition

      let K;

      let v be Element of K;

      :: SIMPLEX0:def3

      attr v is vertex-like means ex S be Subset of K st S is simplex-like & v in S;

    end

    definition

      let K;

      :: SIMPLEX0:def4

      func Vertices K -> Subset of K means

      : Def4: for v be Element of K holds v in it iff v is vertex-like;

      existence

      proof

        set B = { v where v be Element of K : v is vertex-like };

        B c= ( [#] K)

        proof

          let x be object;

          assume x in B;

          then

          consider v be Element of K such that

           A1: x = v and

           A2: v is vertex-like;

          ex S be Subset of K st S is simplex-like & v in S by A2;

          hence thesis by A1;

        end;

        then

        reconsider B as Subset of K;

        take B;

        let v be Element of K;

        hereby

          assume v in B;

          then ex w be Element of K st v = w & w is vertex-like;

          hence v is vertex-like;

        end;

        assume v is vertex-like;

        hence thesis;

      end;

      uniqueness

      proof

        let V1,V2 be Subset of K such that

         A3: for v be Element of K holds v in V1 iff v is vertex-like and

         A4: for v be Element of K holds v in V2 iff v is vertex-like;

        thus for x be object st x in V1 holds x in V2 by A3, A4;

        let x be object;

        assume

         A5: x in V2;

        then

        reconsider v = x as Element of K;

        v is vertex-like by A4, A5;

        hence thesis by A3;

      end;

    end

    definition

      let K be SimplicialComplexStr;

      mode Vertex of K is Element of ( Vertices K);

    end

    definition

      let K be SimplicialComplexStr;

      :: SIMPLEX0:def5

      attr K is finite-vertices means

      : Def5: ( Vertices K) is finite;

    end

    definition

      let K;

      :: SIMPLEX0:def6

      attr K is locally-finite means for v be Vertex of K holds { S where S be Subset of K : S is simplex-like & v in S } is finite;

    end

    definition

      let K;

      :: SIMPLEX0:def7

      attr K is empty-membered means

      : Def7: the topology of K is empty-membered;

      :: SIMPLEX0:def8

      attr K is with_non-empty_elements means

      : Def8: the topology of K is with_non-empty_elements;

    end

    notation

      let K;

      antonym K is with_non-empty_element for K is empty-membered;

      antonym K is with_empty_element for K is with_non-empty_elements;

    end

    definition

      let X;

      :: SIMPLEX0:def9

      mode SimplicialComplexStr of X -> SimplicialComplexStr means

      : Def9: ( [#] it ) c= X;

      existence

      proof

        take the empty TopStruct;

        thus thesis;

      end;

    end

    definition

      let X;

      let KX be SimplicialComplexStr of X;

      :: SIMPLEX0:def10

      attr KX is total means ( [#] KX) = X;

    end

    

     Lm2: ( Vertices K) is empty iff K is empty-membered

    proof

      hereby

        assume

         A1: ( Vertices K) is empty;

        assume K is with_non-empty_element;

        then the topology of K is with_non-empty_element;

        then

        consider D such that

         A2: D in the topology of K;

        reconsider S = D as Subset of K by A2;

         the Element of D in S;

        then

        reconsider v = the Element of D as Element of K;

        S is simplex-like by A2;

        then v is vertex-like;

        hence contradiction by A1, Def4;

      end;

      assume

       A3: K is empty-membered;

      assume ( Vertices K) is non empty;

      then

      consider x be object such that

       A4: x in ( Vertices K);

      reconsider x as Element of K by A4;

      x is vertex-like by A4, Def4;

      then

      consider S be Subset of K such that

       A5: S is simplex-like and

       A6: x in S;

      S in the topology of K by A5;

      then the topology of K is with_non-empty_element by A6;

      hence contradiction by A3;

    end;

    

     Lm3: for S be Subset of K st S is simplex-like & x in S holds x in ( Vertices K)

    proof

      let S be Subset of K such that

       A1: S is simplex-like and

       A2: x in S;

      reconsider v = x as Element of K by A2;

      v is vertex-like by A1, A2;

      hence thesis by Def4;

    end;

    

     Lm4: for A be Subset of K st A is simplex-like holds A c= ( Vertices K) by Lm3;

    

     Lm5: ( Vertices K) = ( union the topology of K)

    proof

      hereby

        let x be object such that

         A1: x in ( Vertices K);

        reconsider v = x as Element of K by A1;

        v is vertex-like by A1, Def4;

        then

        consider S be Subset of K such that

         A2: S is simplex-like and

         A3: v in S;

        S in the topology of K by A2;

        hence x in ( union the topology of K) by A3, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union the topology of K);

      then

      consider y such that

       A4: x in y and

       A5: y in the topology of K by TARSKI:def 4;

      reconsider y as Subset of K by A5;

      y is simplex-like by A5;

      hence thesis by A4, Lm3;

    end;

    

     Lm6: K is finite-vertices implies the topology of K is finite

    proof

      ( Vertices K) = ( union the topology of K) by Lm5;

      then

       A1: the topology of K c= ( bool ( Vertices K)) by ZFMISC_1: 82;

      assume K is finite-vertices;

      then ( Vertices K) is finite;

      hence thesis by A1;

    end;

    registration

      cluster with_empty_element -> non void for SimplicialComplexStr;

      coherence by PENCIL_1:def 4;

      cluster with_non-empty_element -> non void for SimplicialComplexStr;

      coherence by PENCIL_1:def 4;

      cluster non void empty-membered -> with_empty_element for SimplicialComplexStr;

      coherence ;

      cluster non void subset-closed -> with_empty_element for SimplicialComplexStr;

      coherence ;

      cluster empty-membered -> subset-closed finite-vertices for SimplicialComplexStr;

      coherence

      proof

        let K;

        assume

         A1: K is empty-membered;

        then

         A2: the topology of K is empty-membered;

        thus K is subset-closed

        proof

          let x, y such that

           A3: x in ( the_family_of K) and

           A4: y c= x;

          x is empty by A2, A3;

          hence thesis by A3, A4;

        end;

        ( Vertices K) is empty by A1, Lm2;

        hence thesis;

      end;

      cluster finite-vertices -> locally-finite finite-degree for SimplicialComplexStr;

      coherence

      proof

        let K;

        assume

         A5: K is finite-vertices;

        then

        reconsider V = ( Vertices K) as finite Subset of K;

        thus K is locally-finite

        proof

          let v be Vertex of K;

          

           A6: { S where S be Subset of K : S is simplex-like & v in S } c= the topology of K

          proof

            let x be object;

            assume x in { S where S be Subset of K : S is simplex-like & v in S };

            then ex S be Subset of K st x = S & S is simplex-like & v in S;

            hence thesis;

          end;

          the topology of K is finite by A5, Lm6;

          hence thesis by A6;

        end;

        thus K is finite-membered

        proof

          let x;

          assume

           A7: x in ( the_family_of K);

          then

          reconsider X = x as Subset of K;

          X is simplex-like by A7;

          then X c= V by Lm4;

          hence thesis;

        end;

        take ( card V);

        let A be finite Subset of K;

        assume A is open;

        hence thesis by Lm4, NAT_1: 43;

      end;

      cluster locally-finite subset-closed -> finite-membered for SimplicialComplexStr;

      coherence

      proof

        let K be SimplicialComplexStr;

        assume

         A8: K is locally-finite subset-closed;

        ( the_family_of K) is finite-membered

        proof

          let x;

          assume

           A9: x in ( the_family_of K);

          then

          reconsider A = x as Subset of K;

          

           A10: K is non void by A9, PENCIL_1:def 4;

          

           A11: A is simplex-like by A9;

          per cases ;

            suppose x is empty;

            hence thesis;

          end;

            suppose x is non empty;

            then

            consider a be object such that

             A12: a in A;

            reconsider a as Element of K by A12;

            a is vertex-like by A11, A12;

            then

            reconsider a as Vertex of K by Def4;

            set Aa = (A \ {a});

            set X = { S where S be Subset of K : a in S & S c= A };

            defpred P[ set, set] means ($1 \ {a}) = $2;

            set Z = { y where y be Element of ( bool Aa) : ex w be Subset of K st P[w, y] & w in X };

            

             A13: ( bool Aa) c= Z

            proof

              let y be object;

              assume

               A14: y in ( bool Aa);

              then

              reconsider B = y as Subset of K by XBOOLE_1: 1;

               not a in B by A14, ZFMISC_1: 56;

              then

               A15: ((B \/ {a}) \ {a}) = B by ZFMISC_1: 117;

              

               A16: {a} c= A by A12, ZFMISC_1: 31;

              Aa c= A by XBOOLE_1: 36;

              then B c= A by A14;

              then

               A17: (B \/ {a}) c= A by A16, XBOOLE_1: 8;

              then

               A18: (B \/ {a}) is Subset of K by XBOOLE_1: 1;

              a in {a} by TARSKI:def 1;

              then a in (B \/ {a}) by XBOOLE_0:def 3;

              then (B \/ {a}) in X by A17, A18;

              hence thesis by A14, A15, A18;

            end;

            set Y = { S where S be Subset of K : S is simplex-like & a in S };

            

             A19: X c= Y

            proof

              let y be object;

              assume y in X;

              then

              consider S be Subset of K such that

               A20: y = S & a in S and

               A21: S c= A;

              S is simplex-like by A8, A10, A11, A21, MATROID0: 1;

              hence thesis by A20;

            end;

            Y is finite by A8;

            then

             A22: X is finite by A19;

            

             A23: for w be Subset of K, x,y be Element of ( bool Aa) st P[w, x] & P[w, y] holds x = y;

            Z is finite from FRAENKEL:sch 28( A22, A23);

            then

             A24: Aa is finite by A13;

            A = (Aa \/ {a}) by A12, ZFMISC_1: 116;

            hence x is finite by A24;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let X;

      cluster empty void empty-membered strict for SimplicialComplexStr of X;

      existence

      proof

        ( [#] TopStruct (# {} , ( {} ( bool {} )) #)) c= X;

        then

        reconsider T = TopStruct (# {} , ( {} ( bool {} )) #) as SimplicialComplexStr of X by Def9;

        take T;

        thus thesis;

      end;

    end

    registration

      let D;

      cluster non empty non void total empty-membered strict for SimplicialComplexStr of D;

      existence

      proof

        reconsider B = ( bool 0 ) as Subset-Family of D by XBOOLE_1: 2, ZFMISC_1: 67;

        ( [#] TopStruct (# D, B #)) c= D;

        then

        reconsider T = TopStruct (# D, B #) as SimplicialComplexStr of D by Def9;

        take T;

        ( [#] T) = D & B is empty-membered;

        hence thesis by PENCIL_1:def 4;

      end;

      cluster non empty total with_empty_element with_non-empty_element finite-vertices subset-closed strict for SimplicialComplexStr of D;

      existence

      proof

        set E = the Element of D;

        reconsider B = ( bool {E}) as Subset-Family of D by ZFMISC_1: 67;

        ( [#] TopStruct (# D, B #)) c= ( [#] D);

        then

        reconsider T = TopStruct (# D, B #) as SimplicialComplexStr of D by Def9;

        take T;

        

         A1: ( Vertices T) c= {E}

        proof

          let x be object such that

           A2: x in ( Vertices T);

          reconsider v = x as Element of T by A2;

          v is vertex-like by A2, Def4;

          then

          consider S be Subset of T such that

           A3: S is simplex-like and

           A4: v in S;

          S in B by A3;

          hence thesis by A4;

        end;

         {E} in B by ZFMISC_1:def 1;

        then B is with_non-empty_element;

        then

         A5: ( [#] T) = D & T is with_non-empty_element;

        thus thesis by A1, A5;

      end;

    end

    registration

      cluster non empty with_empty_element with_non-empty_element finite-vertices subset-closed strict for SimplicialComplexStr;

      existence

      proof

        take the non empty with_empty_element with_non-empty_element finite-vertices subset-closed strict SimplicialComplexStr of the non empty set;

        thus thesis;

      end;

    end

    registration

      let K be with_non-empty_element SimplicialComplexStr;

      cluster ( Vertices K) -> non empty;

      coherence by Lm2;

    end

    registration

      let K be finite-vertices SimplicialComplexStr;

      cluster simplex-like -> finite for Subset-Family of K;

      coherence

      proof

        let S be Subset-Family of K;

        assume S is simplex-like;

        then

         A1: S c= the topology of K by Th14;

        ( Vertices K) = ( union the topology of K) by Lm5;

        then

         A2: the topology of K c= ( bool ( Vertices K)) by ZFMISC_1: 82;

        ( Vertices K) is finite by Def5;

        hence thesis by A1, A2;

      end;

    end

    registration

      let K be finite-membered SimplicialComplexStr;

      cluster simplex-like -> finite-membered for Subset-Family of K;

      coherence

      proof

        let S be Subset-Family of K;

        assume

         A1: S is simplex-like;

        let x;

        assume

         A2: x in S;

        then

        reconsider X = x as Subset of K;

        X is simplex-like by A1, A2;

        then

         A3: X in the topology of K;

        ( the_family_of K) is finite-membered by MATROID0:def 6;

        hence thesis by A3;

      end;

    end

    theorem :: SIMPLEX0:15

    ( Vertices K) is empty iff K is empty-membered by Lm2;

    theorem :: SIMPLEX0:16

    ( Vertices K) = ( union the topology of K) by Lm5;

    theorem :: SIMPLEX0:17

    for S be Subset of K st S is simplex-like holds S c= ( Vertices K) by Lm4;

    theorem :: SIMPLEX0:18

    K is finite-vertices implies the topology of K is finite by Lm6;

    theorem :: SIMPLEX0:19

    

     Th19: the topology of K is finite & K is non finite-vertices implies K is non finite-membered

    proof

      defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in D2;

      set V = ( Vertices K);

      assume that

       A1: the topology of K is finite and

       A2: K is non finite-vertices;

      

       A3: V is infinite by A2;

      

       A4: V = ( union the topology of K) by Lm5;

      

       A5: for x be object st x in V holds ex y be object st y in the topology of K & P[x, y]

      proof

        let x be object;

        assume x in V;

        then ex y st x in y & y in the topology of K by A4, TARSKI:def 4;

        hence thesis;

      end;

      consider f be Function of V, the topology of K such that

       A6: for x be object st x in V holds P[x, (f . x)] from FUNCT_2:sch 1( A5);

      the topology of K is non empty by A2, A4;

      then ( dom f) = V by FUNCT_2:def 1;

      then

      consider x be object such that

       A7: x in ( rng f) and

       A8: (f " {x}) is infinite by A1, A3, CARD_2: 101;

      x in the topology of K by A7;

      then

      reconsider x as Subset of K;

      (f " {x}) c= x

      proof

        let y be object;

        assume

         A9: y in (f " {x});

        then P[y, (f . y)] by A6;

        then (f . y) in {x} & y in (f . y) by A9, FUNCT_1:def 7;

        hence thesis by TARSKI:def 1;

      end;

      then x is non finite by A8;

      then ( the_family_of K) is non finite-membered by A7;

      hence thesis;

    end;

    theorem :: SIMPLEX0:20

    

     Th20: K is subset-closed & the topology of K is finite implies K is finite-vertices

    proof

      assume that

       A1: K is subset-closed and

       A2: the topology of K is finite;

      assume K is non finite-vertices;

      then K is non finite-membered by A2, Th19;

      then ( the_family_of K) is non finite-membered;

      then

      consider x such that

       A3: x in ( the_family_of K) and

       A4: x is non finite;

       {x} c= ( the_family_of K) by A3, ZFMISC_1: 31;

      then ( subset-closed_closure_of {x}) c= ( the_family_of K) by A1, Th3;

      then ( bool x) c= ( the_family_of K) by Th4;

      hence contradiction by A2, A4;

    end;

    begin

    definition

      let X;

      let Y be Subset-Family of X;

      :: SIMPLEX0:def11

      func Complex_of Y -> strict SimplicialComplexStr of X equals TopStruct (# X, ( subset-closed_closure_of Y) #);

      coherence

      proof

        ( [#] TopStruct (# X, ( subset-closed_closure_of Y) #)) = X;

        hence thesis by Def9;

      end;

    end

    registration

      let X;

      let Y be Subset-Family of X;

      cluster ( Complex_of Y) -> total subset-closed;

      coherence ;

    end

    registration

      let X;

      let Y be non empty Subset-Family of X;

      cluster ( Complex_of Y) -> with_empty_element;

      coherence ;

    end

    registration

      let X;

      let Y be finite-membered Subset-Family of X;

      cluster ( Complex_of Y) -> finite-membered;

      coherence ;

    end

    registration

      let X;

      let Y be finite finite-membered Subset-Family of X;

      cluster ( Complex_of Y) -> finite-vertices;

      coherence

      proof

        set C = ( Complex_of Y);

        reconsider Y1 = Y as Subset-Family of ( union Y) by ZFMISC_1: 82;

        ( subset-closed_closure_of Y1) c= ( bool ( union Y));

        then

         A1: ( union the topology of C) c= ( union ( bool ( union Y))) by ZFMISC_1: 77;

        ( union ( bool ( union Y))) = ( union Y) by ZFMISC_1: 81;

        then ( Vertices C) c= ( union Y) by A1, Lm5;

        hence thesis;

      end;

    end

    theorem :: SIMPLEX0:21

    K is subset-closed implies the TopStruct of K = ( Complex_of the topology of K) by Th7;

    definition

      let X;

      mode SimplicialComplex of X is finite-membered subset-closed SimplicialComplexStr of X;

    end

    definition

      let K be non void SimplicialComplexStr;

      mode Simplex of K is simplex-like Subset of K;

    end

    registration

      let K be with_empty_element SimplicialComplexStr;

      cluster empty -> simplex-like for Subset of K;

      coherence

      proof

        let S be Subset of K;

        assume

         A1: S is empty;

        the topology of K is with_empty_element by Def8;

        then S in the topology of K by A1;

        hence thesis;

      end;

      cluster empty for Simplex of K;

      existence

      proof

        ( {} K) is simplex-like;

        hence thesis;

      end;

    end

    registration

      let K be non void finite-membered SimplicialComplexStr;

      cluster finite for Simplex of K;

      existence

      proof

        consider S be object such that

         A1: S in the topology of K by XBOOLE_0:def 1;

        reconsider S as Simplex of K by A1, PRE_TOPC:def 2;

        S is finite;

        hence thesis;

      end;

    end

    begin

    definition

      let K;

      :: SIMPLEX0:def12

      func degree K -> ExtReal means

      : Def12: (for S be finite Subset of K st S is simplex-like holds ( card S) <= (it + 1)) & ex S be Subset of K st S is simplex-like & ( card S) = (it + 1) if K is non void finite-degree,

it = ( - 1) if K is void

      otherwise it = +infty ;

      existence

      proof

        now

          defpred P[ Nat] means for S be finite Subset of K st S is simplex-like holds ( card S) <= $1;

          assume

           A1: K is non void finite-degree;

          then

           A2: ( the_family_of K) is finite-membered by MATROID0:def 6;

          

           A3: ex n be Nat st P[n] by A1;

          consider k be Nat such that

           A4: P[k] and

           A5: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A3);

          take D = (k - 1);

          thus for S be finite Subset of K st S is simplex-like holds ( card S) <= (D + 1) by A4;

          assume

           A6: for S be Subset of K st S is simplex-like holds ( card S) <> (D + 1);

          per cases ;

            suppose

             A7: k = 0 ;

            consider S be object such that

             A8: S in the topology of K by A1, XBOOLE_0:def 1;

            reconsider S as finite Subset of K by A2, A8;

            

             A9: S is simplex-like by A8;

            then ( card S) = 0 by A4, A7;

            hence contradiction by A6, A7, A9;

          end;

            suppose k > 0 ;

            then

            reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

             P[k1]

            proof

              let S be finite Subset of K;

              assume

               A10: S is simplex-like;

              then ( card S) <= (k1 + 1) by A4;

              then ( card S) < (k1 + 1) by A6, A10, XXREAL_0: 1;

              hence thesis by NAT_1: 13;

            end;

            then (k1 + 1) <= k1 by A5;

            hence contradiction by NAT_1: 13;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let D1,D2 be ExtReal;

        now

          assume

           A11: K is non void finite-degree;

          assume

           A12: for S be finite Subset of K st S is simplex-like holds ( card S) <= (D1 + 1);

          given S1 be Subset of K such that

           A13: S1 is simplex-like & ( card S1) = (D1 + 1);

          assume

           A14: for S be finite Subset of K st S is simplex-like holds ( card S) <= (D2 + 1);

          given S2 be Subset of K such that

           A15: S2 is simplex-like & ( card S2) = (D2 + 1);

          

           A16: (D2 + 1) <= (D1 + 1) by A11, A12, A15;

          (D1 + 1) <= (D2 + 1) by A11, A13, A14;

          hence D1 = D2 by A16, XXREAL_0: 1, XXREAL_3: 11;

        end;

        hence thesis;

      end;

      consistency ;

    end

    registration

      let K be finite-degree SimplicialComplexStr;

      cluster (( degree K) + 1) -> natural;

      coherence

      proof

        per cases ;

          suppose K is void;

          

          then (( degree K) + 1) = (( - 1) + 1) by Def12

          .= 0 ;

          hence thesis;

        end;

          suppose K is non void;

          then

          consider S be Subset of K such that

           A1: S is simplex-like and

           A2: ( card S) = (( degree K) + 1) by Def12;

          ( the_family_of K) is finite-membered & S in the topology of K by A1, MATROID0:def 6;

          then S is finite;

          hence thesis by A2;

        end;

      end;

      cluster ( degree K) -> integer;

      coherence

      proof

        ( degree K) = ((( degree K) + 1) - 1) by XXREAL_3: 24;

        hence thesis;

      end;

    end

    theorem :: SIMPLEX0:22

    

     Th22: ( degree K) = ( - 1) iff K is empty-membered

    proof

      per cases ;

        suppose K is void;

        hence thesis by Def12;

      end;

        suppose

         A1: K is non void;

        hereby

          assume

           A2: ( degree K) = ( - 1);

          then

           A3: K is finite-degree by A1, Def12;

          assume K is with_non-empty_element;

          then the topology of K is with_non-empty_element;

          then

          consider S be non empty set such that

           A4: S in the topology of K;

          reconsider S as Subset of K by A4;

          

           A5: S is simplex-like by A4;

          then

          reconsider S as finite Subset of K by A1, A3;

          ( card S) <= (( - 1) + 1) by A1, A2, A3, A5, Def12;

          then ( card S) = 0 ;

          hence contradiction;

        end;

        assume

         A6: K is empty-membered;

        then

        consider S be Subset of K such that

         A7: S is simplex-like and

         A8: ( card S) = (( degree K) + 1) by A1, Def12;

        

         A9: S in the topology of K by A7;

        assume ( degree K) <> ( - 1);

        then ( card S) <> (( - 1) + 1) by A8, XXREAL_3: 11;

        then

         A10: S is non empty;

        the topology of K is empty-membered by A6;

        hence thesis by A9, A10;

      end;

    end;

    theorem :: SIMPLEX0:23

    

     Th23: ( - 1) <= ( degree K)

    proof

      per cases ;

        suppose K is void;

        hence thesis by Def12;

      end;

        suppose

         A1: K is non void finite-degree;

        then

        reconsider d = ( degree K) as Integer;

         0 = (( - 1) + 1) & (d + 1) >= 0 by A1;

        hence thesis by XREAL_1: 6;

      end;

        suppose K is non void non finite-degree;

        hence thesis by Def12;

      end;

    end;

    theorem :: SIMPLEX0:24

    

     Th24: for S be finite Subset of K st S is simplex-like holds ( card S) <= (( degree K) + 1)

    proof

      let S be finite Subset of K such that

       A1: S is simplex-like;

      S in the topology of K by A1;

      then

       A2: K is non void by PENCIL_1:def 4;

      per cases ;

        suppose K is finite-degree;

        hence thesis by A1, A2, Def12;

      end;

        suppose K is non finite-degree;

        then ( degree K) = +infty by A2, Def12;

        then (( degree K) + 1) = +infty by XXREAL_3:def 2;

        hence thesis by XXREAL_0: 3;

      end;

    end;

    theorem :: SIMPLEX0:25

    

     Th25: K is non void or i >= ( - 1) implies (( degree K) <= i iff K is finite-membered & for S be finite Subset of K st S is simplex-like holds ( card S) <= (i + 1))

    proof

      assume

       A1: K is non void or i >= ( - 1);

      per cases ;

        suppose

         A2: K is void;

        then

         A3: for S be finite Subset of K st S is simplex-like holds ( card S) <= (i + 1) by PENCIL_1:def 4;

        K is empty-membered by A2;

        hence thesis by A1, A2, A3, Th22;

      end;

        suppose

         A4: K is non void;

        hereby

          assume

           A5: ( degree K) <= i;

          then

           A6: (( degree K) + 1) <= (i + 1) by XXREAL_3: 35;

          i in REAL by XREAL_0:def 1;

          then

           A7: ( degree K) <> +infty by A5, XXREAL_0: 9;

          then K is finite-degree or K is empty-membered by Def12;

          hence K is finite-membered;

          let S be finite Subset of K;

          assume

           A8: S is simplex-like;

          K is non void finite-degree or K is void by A7, Def12;

          then ( card S) <= (( degree K) + 1) by A4, A8, Def12;

          hence ( card S) <= (i + 1) by A6, XXREAL_0: 2;

        end;

        assume that

         A9: K is finite-membered and

         A10: for S be finite Subset of K st S is simplex-like holds ( card S) <= (i + 1);

        consider S be object such that

         A11: S in the topology of K by A4, XBOOLE_0:def 1;

        reconsider S as Subset of K by A11;

        

         A12: S is simplex-like by A11;

        then

        reconsider S as finite Subset of K by A9;

        ( card S) <= (i + 1) by A10, A12;

        then

        reconsider i1 = (i + 1) as Element of NAT by INT_1: 3;

        for A be finite Subset of K st A is open holds ( card A) <= i1 by A10;

        then

         A13: K is finite-degree by A9;

        then

        reconsider d = ( degree K) as Integer;

        ex S1 be Subset of K st S1 is simplex-like & ( card S1) = (( degree K) + 1) by A4, A13, Def12;

        then (d + 1) <= (i + 1) by A9, A10;

        hence thesis by XREAL_1: 6;

      end;

    end;

    theorem :: SIMPLEX0:26

    for A be finite Subset of X holds ( degree ( Complex_of {A})) = (( card A) - 1)

    proof

      let A be finite Subset of X;

      set C = ( Complex_of {A});

      

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

      then for S be finite Subset of C st S is simplex-like holds ( card S) <= ((( card A) - 1) + 1) by NAT_1: 43;

      then

       A2: ( degree C) <= (( card A) - 1) by Th25;

      A c= A;

      then

      reconsider A1 = A as finite Simplex of C by A1, PRE_TOPC:def 2;

      ( card A) = ((( card A) - 1) + 1) & ( card A1) <= (( degree C) + 1) by Def12;

      then (( card A) - 1) <= ( degree C) by XREAL_1: 8;

      hence (( card A) - 1) = ( degree C) by A2, XXREAL_0: 1;

    end;

    begin

    definition

      let X;

      let KX be SimplicialComplexStr of X;

      :: SIMPLEX0:def13

      mode SubSimplicialComplex of KX -> SimplicialComplex of X means

      : Def13: ( [#] it ) c= ( [#] KX) & the topology of it c= the topology of KX;

      existence

      proof

        set T = TopStruct (# 0 , ( {} ( bool 0 )) #);

        ( the_family_of T) is empty & ( [#] T) c= X;

        then

        reconsider T = TopStruct (# 0 , ( {} ( bool 0 )) #) as SimplicialComplex of X by Def9, MATROID0:def 3, MATROID0:def 6;

        take T;

        thus thesis;

      end;

    end

    reserve KX for SimplicialComplexStr of X,

SX for SubSimplicialComplex of KX;

    registration

      let X, KX;

      cluster empty void strict for SubSimplicialComplex of KX;

      existence

      proof

        set C = ( Complex_of ( {} ( bool {} )));

        

         A1: ( [#] C) c= ( [#] KX) & the topology of C c= the topology of KX;

        ( [#] C) c= X;

        then C is SimplicialComplexStr of X by Def9;

        then

        reconsider C as SubSimplicialComplex of KX by A1, Def13;

        take C;

        thus thesis;

      end;

    end

    registration

      let X;

      let KX be void SimplicialComplexStr of X;

      cluster -> void for SubSimplicialComplex of KX;

      coherence

      proof

        let S be SubSimplicialComplex of KX;

        the topology of S c= the topology of KX & the topology of KX is empty by Def13, PENCIL_1:def 4;

        hence thesis;

      end;

    end

    registration

      let D;

      let KD be non void subset-closed SimplicialComplexStr of D;

      cluster non void for SubSimplicialComplex of KD;

      existence

      proof

        

         A1: ( the_family_of KD) is subset-closed;

        consider x be object such that

         A2: x in the topology of KD by XBOOLE_0:def 1;

        reconsider x as set by TARSKI: 1;

        per cases ;

          suppose x is empty;

          then

          reconsider x as empty Subset of KD by A2;

          set S = ( Complex_of {x});

          

           A3: ( [#] S) = ( [#] KD);

          ( [#] KD) c= D by Def9;

          then

          reconsider S as SimplicialComplex of D by A3, Def9;

          take S;

           {x} c= the topology of KD by A2, ZFMISC_1: 31;

          then ( subset-closed_closure_of {x}) c= the topology of KD by A1, Th3;

          hence thesis by A3, Def13;

        end;

          suppose

           A4: x is non empty;

          set d = the Element of x;

          d in x by A4;

          then

          reconsider dd = {d} as Subset of KD by A2, ZFMISC_1: 31;

          set S = ( Complex_of {dd});

          

           A5: ( [#] S) = ( [#] KD);

          ( [#] KD) c= D by Def9;

          then

          reconsider S as SimplicialComplex of D by A5, Def9;

          take S;

          dd c= x by A4, ZFMISC_1: 31;

          then dd in the topology of KD by A1, A2;

          then {dd} c= the topology of KD by ZFMISC_1: 31;

          then the topology of S c= the topology of KD by A1, Th3;

          hence thesis by A5, Def13;

        end;

      end;

    end

    registration

      let X;

      let KX be finite-vertices SimplicialComplexStr of X;

      cluster -> finite-vertices for SubSimplicialComplex of KX;

      coherence

      proof

        let SX be SubSimplicialComplex of KX;

        

         A1: ( Vertices KX) is finite by Def5;

        the topology of SX c= the topology of KX by Def13;

        then

         A2: ( union the topology of SX) c= ( union the topology of KX) by ZFMISC_1: 77;

        ( union the topology of SX) = ( Vertices SX) & ( union the topology of KX) = ( Vertices KX) by Lm5;

        hence thesis by A2, A1;

      end;

    end

    registration

      let X;

      let KX be finite-degree SimplicialComplexStr of X;

      cluster -> finite-degree for SubSimplicialComplex of KX;

      coherence

      proof

        let S be SubSimplicialComplex of KX;

        consider n be Nat such that

         A1: for A be finite Subset of KX st A is simplex-like holds ( card A) <= n by MATROID0:def 7;

        thus S is finite-membered;

        take n;

        let A be finite Subset of S;

        assume A is simplex-like;

        then

         A2: A in the topology of S;

        ( [#] S) c= ( [#] KX) by Def13;

        then

        reconsider A1 = A as finite Subset of KX by XBOOLE_1: 1;

        the topology of S c= the topology of KX by Def13;

        then A1 is simplex-like by A2;

        hence thesis by A1;

      end;

    end

    theorem :: SIMPLEX0:27

    

     Th27: for S1 be SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX

    proof

      let S1 be SubSimplicialComplex of SX;

      ( [#] SX) c= ( [#] KX) & ( [#] S1) c= ( [#] SX) by Def13;

      then

       A1: ( [#] S1) c= ( [#] KX);

      the topology of SX c= the topology of KX & the topology of S1 c= the topology of SX by Def13;

      then the topology of S1 c= the topology of KX;

      hence thesis by A1, Def13;

    end;

    theorem :: SIMPLEX0:28

    

     Th28: for A be Subset of KX holds for S be finite-membered Subset-Family of A st ( subset-closed_closure_of S) c= the topology of KX holds ( Complex_of S) is strict SubSimplicialComplex of KX

    proof

      let A be Subset of KX;

      let S be finite-membered Subset-Family of A such that

       A1: ( subset-closed_closure_of S) c= the topology of KX;

      set C = ( Complex_of S);

      ( [#] KX) c= X by Def9;

      then ( [#] C) c= X;

      then ( [#] C) c= ( [#] KX) & C is strict SimplicialComplexStr of X by Def9;

      hence thesis by A1, Def13;

    end;

    theorem :: SIMPLEX0:29

    for KX be subset-closed SimplicialComplexStr of X holds for A be Subset of KX holds for S be finite-membered Subset-Family of A st S c= the topology of KX holds ( Complex_of S) is strict SubSimplicialComplex of KX

    proof

      let KX be subset-closed SimplicialComplexStr of X;

      let A be Subset of KX;

      let S be finite-membered Subset-Family of A;

      

       A1: ( the_family_of KX) is subset-closed;

      assume S c= the topology of KX;

      hence thesis by A1, Th3, Th28;

    end;

    theorem :: SIMPLEX0:30

    for Y1,Y2 be Subset-Family of X st Y1 is finite-membered & Y1 is_finer_than Y2 holds ( Complex_of Y1) is SubSimplicialComplex of ( Complex_of Y2)

    proof

      let Y1,Y2 be Subset-Family of X such that

       A1: Y1 is finite-membered and

       A2: Y1 is_finer_than Y2;

      set C1 = ( Complex_of Y1), C2 = ( Complex_of Y2);

      

       A3: ( [#] C1) = X & ( [#] C2) = X;

      ( subset-closed_closure_of Y1) c= ( subset-closed_closure_of Y2) by A2, Th6;

      hence thesis by A1, A3, Def13;

    end;

    theorem :: SIMPLEX0:31

    ( Vertices SX) c= ( Vertices KX)

    proof

      let x be object;

      assume

       A1: x in ( Vertices SX);

      then

      reconsider v = x as Element of SX;

      v is vertex-like by A1, Def4;

      then

      consider S be Subset of SX such that

       A2: S is simplex-like and

       A3: v in S;

      

       A4: the topology of SX c= the topology of KX by Def13;

      

       A5: S in the topology of SX by A2;

      then S in the topology of KX by A4;

      then

      reconsider S as Subset of KX;

      v in S by A3;

      then

      reconsider v as Element of KX;

      S is simplex-like by A4, A5;

      then v is vertex-like by A3;

      hence thesis by Def4;

    end;

    theorem :: SIMPLEX0:32

    

     Th32: ( degree SX) <= ( degree KX)

    proof

      per cases ;

        suppose

         A1: SX is non finite-degree;

        SX is non void

        proof

          assume SX is void;

          then SX is empty-membered;

          hence contradiction by A1;

        end;

        then KX is non finite-degree non void & ( degree SX) = +infty by A1, Def12;

        hence thesis by Def12;

      end;

        suppose SX is void;

        then ( degree SX) = ( - 1) by Def12;

        hence thesis by Th23;

      end;

        suppose

         A2: SX is non void finite-degree;

        then

         A3: KX is non void;

        per cases ;

          suppose KX is non finite-degree;

          then ( degree KX) = +infty by A3, Def12;

          hence thesis by XXREAL_0: 3;

        end;

          suppose

           A4: KX is finite-degree;

          

           A5: the topology of SX c= the topology of KX by Def13;

          consider S be Subset of SX such that

           A6: S is simplex-like and

           A7: ( card S) = (( degree SX) + 1) by A2, Def12;

          

           A8: S in the topology of SX by A6;

          then S in the topology of KX by A5;

          then

          reconsider S1 = S as finite Subset of KX by A4, A7;

          S1 is simplex-like by A5, A8;

          then (( degree SX) + 1) <= (( degree KX) + 1) by A3, A4, A7, Def12;

          then

           A9: ((( degree SX) + 1) - 1) <= ((( degree KX) + 1) - 1) by XXREAL_3: 37;

          ((( degree SX) + 1) - 1) = ( degree SX) by XXREAL_3: 24;

          hence thesis by A9, XXREAL_3: 24;

        end;

      end;

    end;

    definition

      let X, KX, SX;

      :: SIMPLEX0:def14

      attr SX is maximal means

      : Def14: for A be Subset of SX st A in the topology of KX holds A is simplex-like;

    end

    theorem :: SIMPLEX0:33

    

     Th33: SX is maximal iff (( bool ( [#] SX)) /\ the topology of KX) c= the topology of SX

    proof

      hereby

        assume

         A1: SX is maximal;

        thus (( bool ( [#] SX)) /\ the topology of KX) c= the topology of SX

        proof

          let x be object;

          assume

           A2: x in (( bool ( [#] SX)) /\ the topology of KX);

          then

          reconsider A = x as Subset of SX by XBOOLE_0:def 4;

          A in the topology of KX by A2, XBOOLE_0:def 4;

          then A is simplex-like by A1;

          hence thesis;

        end;

      end;

      assume

       A3: (( bool ( [#] SX)) /\ the topology of KX) c= the topology of SX;

      let A be Subset of SX;

      assume A in the topology of KX;

      then A in (( bool ( [#] SX)) /\ the topology of KX) by XBOOLE_0:def 4;

      hence thesis by A3;

    end;

    registration

      let X, KX;

      cluster maximal strict for SubSimplicialComplex of KX;

      existence

      proof

        set B = (( bool {} ) /\ the topology of KX);

        reconsider B as finite-membered subset-closed Subset-Family of ( {} KX) by XBOOLE_1: 17, ZFMISC_1: 1, ZFMISC_1: 33;

        ( subset-closed_closure_of B) = B by Th7;

        then

        reconsider C = ( Complex_of B) as strict SubSimplicialComplex of KX by Th28, XBOOLE_1: 17;

        take C;

        C = TopStruct (# ( {} KX), B #) & ( bool ( [#] C)) = ( bool {} ) by Th7;

        hence thesis by Th33;

      end;

    end

    theorem :: SIMPLEX0:34

    

     Th34: for S1 be SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds S1 is maximal SubSimplicialComplex of KX

    proof

      let S1 be SubSimplicialComplex of SX;

      reconsider s1 = S1 as SubSimplicialComplex of KX by Th27;

      assume that

       A1: SX is maximal and

       A2: S1 is maximal;

      

       A3: ( [#] S1) c= ( [#] SX) by Def13;

      now

        let A be Subset of s1;

        reconsider a = A as Subset of SX by A3, XBOOLE_1: 1;

        assume A in the topology of KX;

        then a is simplex-like by A1;

        then a in the topology of SX;

        hence A is simplex-like by A2;

      end;

      hence S1 is maximal SubSimplicialComplex of KX by Def14;

    end;

    theorem :: SIMPLEX0:35

    for S1 be SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds S1 is maximal

    proof

      let S1 be SubSimplicialComplex of SX;

      assume S1 is maximal SubSimplicialComplex of KX;

      then

      reconsider s1 = S1 as maximal SubSimplicialComplex of KX;

      the topology of SX c= the topology of KX by Def13;

      then

       A1: (( bool ( [#] s1)) /\ the topology of SX) c= (( bool ( [#] s1)) /\ the topology of KX) by XBOOLE_1: 26;

      (( bool ( [#] s1)) /\ the topology of KX) c= the topology of s1 by Th33;

      then (( bool ( [#] S1)) /\ the topology of SX) c= the topology of S1 by A1;

      hence thesis by Th33;

    end;

    theorem :: SIMPLEX0:36

    

     Th36: for K1,K2 be maximal SubSimplicialComplex of KX st ( [#] K1) = ( [#] K2) holds the TopStruct of K1 = the TopStruct of K2

    proof

      let K1,K2 be maximal SubSimplicialComplex of KX;

      assume

       A1: ( [#] K1) = ( [#] K2);

      set TOP1 = the topology of K1, TOP2 = the topology of K2, TOP = the topology of KX;

      

       A2: (TOP /\ ( bool ( [#] K2))) c= TOP2 by Th33;

      TOP1 c= TOP by Def13;

      then

       A3: TOP1 c= (TOP /\ ( bool ( [#] K1))) by XBOOLE_1: 19;

      TOP2 c= TOP by Def13;

      then

       A4: TOP2 c= (TOP /\ ( bool ( [#] K2))) by XBOOLE_1: 19;

      (TOP /\ ( bool ( [#] K1))) c= TOP1 by Th33;

      

      then TOP1 = (TOP /\ ( bool ( [#] K1))) by A3

      .= TOP2 by A1, A2, A4;

      hence thesis by A1;

    end;

    definition

      let X;

      let KX be subset-closed SimplicialComplexStr of X;

      let A be Subset of KX;

      :: SIMPLEX0:def15

      func KX | A -> maximal strict SubSimplicialComplex of KX means

      : Def15: ( [#] it ) = A;

      existence

      proof

        ( the_family_of KX) is subset-closed;

        then

        reconsider BA = (( bool A) /\ the topology of KX) as finite-membered subset-closed Subset-Family of A by A1, XBOOLE_1: 17;

        set KA = TopStruct (# A, BA #);

        

         A2: ( [#] KA) c= ( [#] KX) & the topology of KA c= the topology of KX by XBOOLE_1: 17;

        

         A3: KA is subset-closed finite-membered;

        ( [#] KX) c= X by Def9;

        then ( [#] KA) c= X;

        then KA is SimplicialComplexStr of X by Def9;

        then

        reconsider KA as maximal strict SubSimplicialComplex of KX by A2, A3, Def13, Th33;

        take KA;

        thus thesis;

      end;

      uniqueness by Th36;

    end

    reserve SC for SimplicialComplex of X;

    definition

      let X, SC;

      let A be Subset of SC;

      :: original: |

      redefine

      :: SIMPLEX0:def16

      func SC | A means

      : Def16: ( [#] it ) = A;

      compatibility

      proof

        let KA be maximal strict SubSimplicialComplex of SC;

        ( the_family_of SC) is finite-membered & (( bool A) /\ the topology of SC) c= the topology of SC by MATROID0:def 6, XBOOLE_1: 17;

        hence thesis by Def15;

      end;

    end

    theorem :: SIMPLEX0:37

    

     Th37: for A be Subset of SC holds the topology of (SC | A) = (( bool A) /\ the topology of SC)

    proof

      let A be Subset of SC;

      

       A1: ( [#] (SC | A)) = A by Def16;

      then

       A2: (( bool A) /\ the topology of SC) c= the topology of (SC | A) by Th33;

      the topology of (SC | A) c= the topology of SC by Def13;

      then the topology of (SC | A) c= (( bool A) /\ the topology of SC) by A1, XBOOLE_1: 19;

      hence thesis by A2;

    end;

    theorem :: SIMPLEX0:38

    for A,B be Subset of SC holds for B1 be Subset of (SC | A) st B1 = B holds ((SC | A) | B1) = (SC | B)

    proof

      let A,B be Subset of SC;

      let B1 be Subset of (SC | A);

      reconsider SCAB = ((SC | A) | B1) as maximal strict SubSimplicialComplex of SC by Th34;

      assume

       A1: B1 = B;

      ( [#] SCAB) = B1 by Def16;

      hence thesis by A1, Def16;

    end;

    theorem :: SIMPLEX0:39

    (SC | ( [#] SC)) = the TopStruct of SC

    proof

      set T = the TopStruct of SC;

      

       A1: ( [#] T) c= ( [#] SC) & (( bool ( [#] T)) /\ the topology of SC) = the topology of SC by XBOOLE_1: 28;

      ( the_family_of SC) = ( the_family_of T) & ( the_family_of SC) is finite-membered subset-closed by MATROID0:def 6;

      then

       A2: T is finite-membered subset-closed;

      ( [#] SC) c= X by Def9;

      then ( [#] T) c= X;

      then T is SimplicialComplexStr of X by Def9;

      then

      reconsider T as maximal SubSimplicialComplex of SC by A1, A2, Def13, Th33;

      ( [#] T) = ( [#] SC);

      hence thesis by Def16;

    end;

    theorem :: SIMPLEX0:40

    for A,B be Subset of SC st A c= B holds (SC | A) is SubSimplicialComplex of (SC | B)

    proof

      let A,B be Subset of SC;

      

       A1: (( bool A) /\ the topology of SC) = the topology of (SC | A) & (( bool B) /\ the topology of SC) = the topology of (SC | B) by Th37;

      assume

       A2: A c= B;

      then ( bool A) c= ( bool B) by ZFMISC_1: 67;

      then

       A3: (( bool A) /\ the topology of SC) c= (( bool B) /\ the topology of SC) by XBOOLE_1: 27;

      ( [#] (SC | A)) = A & ( [#] (SC | B)) = B by Def16;

      hence thesis by A2, A3, A1, Def13;

    end;

    begin

    definition

      let X, KX;

      let i be dim-like number;

      :: SIMPLEX0:def17

      func Skeleton_of (KX,i) -> SimplicialComplexStr of X equals ( Complex_of ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)));

      coherence

      proof

        set C = ( Complex_of ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)));

        ( [#] KX) c= X by Def9;

        then ( [#] C) c= X;

        hence thesis by Def9;

      end;

    end

    definition

      let n be natural Number;

      :: original: -

      redefine

      func - n -> integer number ;

      coherence by TARSKI: 1;

    end

    registration

      let X, KX;

      cluster ( Skeleton_of (KX,( - 1))) -> empty-membered;

      coherence

      proof

        assume ( Skeleton_of (KX,( - 1))) is with_non-empty_element;

        then the topology of ( Skeleton_of (KX,( - 1))) is with_non-empty_element;

        then

        consider x be non empty set such that

         A1: x in the topology of ( Skeleton_of (KX,( - 1)));

        consider b be set such that

         A2: x c= b and

         A3: b in ( the_subsets_with_limited_card (( Segm (( - 1) + 1)),the topology of KX)) by A1, Th2;

        ( card b) c= ( card ( Segm (( - 1) + 1))) by A3, Def2;

        then ( card b) c= {} ;

        then b is empty;

        hence thesis by A2;

      end;

      let i be dim-like number;

      cluster ( Skeleton_of (KX,i)) -> finite-degree;

      coherence

      proof

        reconsider i1 = (i + 1) as Nat;

        set SUB = ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX));

        set C = ( Complex_of SUB);

        now

          let A be finite Subset of C;

          assume A is open;

          then A in ( subset-closed_closure_of SUB);

          then

          consider B be set such that

           A4: A c= B & B in SUB by Th2;

          ( card A) c= ( card B) & ( card B) c= i1 by A4, Def2, CARD_1: 11;

          then ( Segm ( card A)) c= ( Segm i1);

          hence ( card A) <= i1 by NAT_1: 39;

        end;

        hence thesis;

      end;

    end

    registration

      let X;

      let KX be empty-membered SimplicialComplexStr of X;

      let i be dim-like number;

      cluster ( Skeleton_of (KX,i)) -> empty-membered;

      coherence

      proof

        assume ( Skeleton_of (KX,i)) is with_non-empty_element;

        then the topology of ( Skeleton_of (KX,i)) is with_non-empty_element;

        then

        consider x be non empty set such that

         A1: x in the topology of ( Skeleton_of (KX,i));

        

         A2: the topology of KX is empty-membered by Def7;

        consider y such that

         A3: x c= y and

         A4: y in ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)) by A1, Th2;

        y in the topology of KX by A4, Def2;

        then y is empty by A2;

        hence thesis by A3;

      end;

    end

    registration

      let D;

      let KD be non void subset-closed SimplicialComplexStr of D;

      let i be dim-like number;

      cluster ( Skeleton_of (KD,i)) -> non void;

      coherence

      proof

        reconsider E = {} as Subset of KD by XBOOLE_1: 2;

        E in the topology of KD & ( card E) c= ( card ( Segm (i + 1))) by PRE_TOPC:def 2;

        then E in ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KD)) by Def2;

        hence thesis;

      end;

    end

    theorem :: SIMPLEX0:41

    for i1,i2 be dim-like number st ( - 1) <= i1 & i1 <= i2 holds ( Skeleton_of (KX,i1)) is SubSimplicialComplex of ( Skeleton_of (KX,i2))

    proof

      let i1,i2 be dim-like number;

      assume that ( - 1) <= i1 and

       A1: i1 <= i2;

      reconsider I1 = (i1 + 1), I2 = (i2 + 1) as Element of NAT by INT_1: 3;

      ( the_subsets_with_limited_card (( Segm (i1 + 1)),the topology of KX)) c= ( the_subsets_with_limited_card (( Segm (i2 + 1)),the topology of KX))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        I1 <= I2 by A1, XREAL_1: 6;

        then

         A2: ( card ( Segm I1)) c= ( card ( Segm I2)) by NAT_1: 40;

        assume

         A3: x in ( the_subsets_with_limited_card (( Segm (i1 + 1)),the topology of KX));

        then ( card xx) c= ( card I1) by Def2;

        then

         A4: ( card xx) c= ( card I2) by A2;

        x in the topology of KX by A3, Def2;

        hence thesis by A4, Def2;

      end;

      then ( the_subsets_with_limited_card (( Segm (i1 + 1)),the topology of KX)) is_finer_than ( the_subsets_with_limited_card (( Segm (i2 + 1)),the topology of KX));

      then

       A5: the topology of ( Skeleton_of (KX,i1)) c= the topology of ( Skeleton_of (KX,i2)) by Th6;

      ( [#] ( Skeleton_of (KX,i1))) = ( [#] ( Skeleton_of (KX,i2)));

      hence thesis by A5, Def13;

    end;

    definition

      let X;

      let KX be subset-closed SimplicialComplexStr of X;

      let i be dim-like number;

      :: original: Skeleton_of

      redefine

      func Skeleton_of (KX,i) -> SubSimplicialComplex of KX ;

      coherence

      proof

        

         A1: ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)) c= the topology of KX by Def2;

        ( the_family_of KX) is subset-closed;

        then ( [#] ( Skeleton_of (KX,i))) = ( [#] KX) & ( subset-closed_closure_of ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX))) c= the topology of KX by A1, Th3;

        hence thesis by Def13;

      end;

    end

    theorem :: SIMPLEX0:42

    for i be dim-like number st KX is subset-closed & ( Skeleton_of (KX,i)) is empty-membered holds KX is empty-membered or i = ( - 1)

    proof

      let i be dim-like number;

      assume KX is subset-closed;

      then

       A1: ( the_family_of KX) is subset-closed;

      assume

       A2: ( Skeleton_of (KX,i)) is empty-membered;

      assume KX is with_non-empty_element;

      then the topology of KX is with_non-empty_element;

      then

      consider x be non empty set such that

       A3: x in the topology of KX;

      consider y be object such that

       A4: y in x by XBOOLE_0:def 1;

      assume i <> ( - 1);

      then {} c= ( card ( Segm (i + 1))) & ( Segm (i + 1)) is non empty;

      then {} in ( card ( Segm (i + 1))) by CARD_1: 3;

      then 1 c= ( card ( Segm (i + 1))) by CARD_2: 68;

      then

       A5: ( card {y}) c= ( card ( Segm (i + 1))) by CARD_1: 30;

       {y} c= x by A4, ZFMISC_1: 31;

      then {y} in the topology of KX by A1, A3;

      then {y} in ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)) by A5, Def2;

      then

       A6: {y} in the topology of ( Skeleton_of (KX,i)) by Th2;

      the topology of ( Skeleton_of (KX,i)) is empty-membered by A2;

      hence thesis by A6;

    end;

    theorem :: SIMPLEX0:43

    for i be dim-like number holds ( degree ( Skeleton_of (KX,i))) <= ( degree KX)

    proof

      let i be dim-like number;

      set S = ( Skeleton_of (KX,i));

      per cases ;

        suppose KX is void or S is void;

        then KX is empty-membered or S is empty-membered;

        then ( degree ( Skeleton_of (KX,i))) = ( - 1) by Th22;

        hence thesis by Th23;

      end;

        suppose

         A1: KX is non void finite-degree & S is non void;

        then

        reconsider d = ( degree KX) as Integer;

        now

          let s be finite Subset of S;

          assume s is simplex-like;

          then s in ( subset-closed_closure_of ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)));

          then

          consider a be set such that

           A2: s c= a and

           A3: a in ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)) by Th2;

          

           A4: a in the topology of KX by A3, Def2;

          reconsider a as finite Subset of KX by A3;

          ( Segm ( card s)) c= ( Segm ( card a)) by A2, CARD_1: 11;

          then

           A5: ( card s) <= ( card a) by NAT_1: 39;

          a is simplex-like & KX is non void by A4, PENCIL_1:def 4;

          then ( card a) <= (d + 1) by Th25;

          hence ( card s) <= (d + 1) by A5, XXREAL_0: 2;

        end;

        hence thesis by A1, Th25;

      end;

        suppose

         A6: KX is non finite-degree;

        KX is non void

        proof

          assume KX is void;

          then KX is empty-membered;

          hence thesis by A6;

        end;

        then ( degree KX) = +infty by A6, Def12;

        hence thesis by XXREAL_0: 3;

      end;

    end;

    theorem :: SIMPLEX0:44

    for i be dim-like number st ( - 1) <= i holds ( degree ( Skeleton_of (KX,i))) <= i

    proof

      let i be dim-like number;

      set swlc = ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX));

      set S = ( Skeleton_of (KX,i));

      assume

       A1: ( - 1) <= i;

      reconsider i1 = (i + 1) as Element of NAT by INT_1: 3;

      now

        let A be finite Subset of S;

        assume A is simplex-like;

        then A in the topology of S;

        then

        consider x such that

         A2: A c= x & x in swlc by Th2;

        ( card x) c= ( card ( Segm (i + 1))) & ( card A) c= ( card x) by A2, Def2, CARD_1: 11;

        then

         A3: ( card A) c= ( card ( Segm i1));

        ( card ( Segm ( card A))) = ( card A);

        hence ( card A) <= (i + 1) by A3, NAT_1: 40;

      end;

      hence thesis by A1, Th25;

    end;

    theorem :: SIMPLEX0:45

    for i be dim-like number st ( - 1) <= i & ( Skeleton_of (KX,i)) = the TopStruct of KX holds ( degree KX) <= i

    proof

      let i be dim-like number;

      assume

       A1: ( - 1) <= i;

      per cases ;

        suppose KX is empty-membered;

        hence thesis by A1, Th22;

      end;

        suppose

         A2: KX is with_non-empty_element;

        reconsider i1 = (i + 1) as Element of NAT by INT_1: 3;

        assume

         A3: ( Skeleton_of (KX,i)) = the TopStruct of KX;

         A4:

        now

          let S be finite Subset of KX;

          assume S is simplex-like;

          then S in ( subset-closed_closure_of ( the_subsets_with_limited_card (i1,the topology of KX))) by A3;

          then

          consider y such that

           A5: S c= y & y in ( the_subsets_with_limited_card (i1,the topology of KX)) by Th2;

          ( card S) c= ( card y) & ( card y) c= ( card i1) by A5, Def2, CARD_1: 11;

          then

           A6: ( card S) c= ( card ( Segm i1));

          ( card S) = ( card ( Segm ( card S)));

          hence ( card S) <= i1 by A6, NAT_1: 40;

        end;

        for x st x in the topology of KX holds x is finite by A3;

        then ( the_family_of KX) is finite-membered;

        then KX is finite-membered;

        hence thesis by A2, A4, Th25;

      end;

    end;

    theorem :: SIMPLEX0:46

    for i be dim-like number st KX is subset-closed & ( degree KX) <= i holds ( Skeleton_of (KX,i)) = the TopStruct of KX

    proof

      let i be dim-like number;

      assume that

       A1: KX is subset-closed and

       A2: ( degree KX) <= i;

      set S = ( Skeleton_of (KX,i));

      i in REAL by XREAL_0:def 1;

      then ( degree KX) < +infty by A2, XXREAL_0: 2, XXREAL_0: 9;

      then

       A3: KX is finite-degree or KX is empty-membered by Def12;

      then

       A4: ( the_family_of KX) is finite-membered by MATROID0:def 6;

      

       A5: the topology of KX c= the topology of S

      proof

        let x be object;

        

         A6: (( degree KX) + 1) <= (i + 1) by A2, XXREAL_3: 36;

        assume

         A7: x in the topology of KX;

        then

        reconsider A = x as finite Subset of KX by A4;

        A is simplex-like & KX is non void by A7, PENCIL_1:def 4;

        then ( card A) <= (( degree KX) + 1) by A3, Def12;

        then ( card A) <= (i + 1) & (i + 1) in NAT by A6, INT_1: 3, XXREAL_0: 2;

        then ( card ( Segm ( card A))) c= ( card ( Segm (i + 1))) by NAT_1: 40;

        then A in ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)) by A7, Def2;

        hence thesis by Th2;

      end;

      

       A8: ( the_subsets_with_limited_card (( Segm (i + 1)),the topology of KX)) c= the topology of KX by Def2;

      ( the_family_of KX) is subset-closed by A1;

      then the topology of S c= the topology of KX by A8, Th3;

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    reserve K for non void subset-closed SimplicialComplexStr;

    

     Lm7: ( - 1) <= i & i <= ( degree K) implies ex S be Simplex of K st ( card S) = (i + 1)

    proof

      assume that

       A1: ( - 1) <= i and

       A2: i <= ( degree K);

      (( - 1) + 1) <= (i + 1) by A1, XREAL_1: 6;

      then

      reconsider i1 = (i + 1) as Element of NAT by INT_1: 3;

      per cases ;

        suppose

         A3: not K is finite-degree;

        per cases by A3;

          suppose not K is finite-membered;

          then not ( the_family_of K) is finite-membered;

          then

          consider A be set such that

           A4: A in ( the_family_of K) and

           A5: A is infinite;

          ( card i1) c= ( card A) by A5;

          then

          consider f be Function such that

           A6: f is one-to-one & ( dom f) = i1 and

           A7: ( rng f) c= A by CARD_1: 10;

          ( rng f) in ( the_family_of K) by A4, A7, CLASSES1:def 1;

          then

          reconsider R = ( rng f) as Simplex of K by PRE_TOPC:def 2;

          take R;

          (R,i1) are_equipotent by A6, WELLORD2:def 4;

          hence thesis by CARD_1:def 2;

        end;

          suppose for n be Nat holds ex A be finite Subset of K st A is open & ( card A) > n;

          then

          consider A be finite Subset of K such that

           A8: A is simplex-like and

           A9: ( card A) > i1;

          ( card ( Segm i1)) in ( card ( Segm ( card A))) by A9, NAT_1: 41;

          then ( card i1) c= ( card A) by CARD_1: 3;

          then

          consider f be Function such that

           A10: f is one-to-one & ( dom f) = i1 and

           A11: ( rng f) c= A by CARD_1: 10;

          A in ( the_family_of K) by A8;

          then ( rng f) in ( the_family_of K) by A11, CLASSES1:def 1;

          then

          reconsider R = ( rng f) as Simplex of K by PRE_TOPC:def 2;

          take R;

          (R,i1) are_equipotent by A10, WELLORD2:def 4;

          hence thesis by CARD_1:def 2;

        end;

      end;

        suppose

         A12: K is finite-degree;

        then

        reconsider d = ( degree K) as Integer;

        consider S be Subset of K such that

         A13: S is simplex-like and

         A14: ( card S) = (( degree K) + 1) by A12, Def12;

        reconsider s = S as finite Subset of K by A12, A13;

        (i + 1) <= (d + 1) by A2, XREAL_1: 6;

        then ( Segm i1) c= ( Segm ( card s)) by A14, NAT_1: 39;

        then ( card i1) c= ( card ( card s));

        then

        consider f be Function such that

         A15: f is one-to-one & ( dom f) = i1 and

         A16: ( rng f) c= S by CARD_1: 10;

        S in ( the_family_of K) by A13;

        then ( rng f) in ( the_family_of K) by A16, CLASSES1:def 1;

        then

        reconsider R = ( rng f) as Simplex of K by PRE_TOPC:def 2;

        take R;

        (R,i1) are_equipotent by A15, WELLORD2:def 4;

        hence thesis by CARD_1:def 2;

      end;

    end;

    definition

      let K;

      let i be Real;

      :: SIMPLEX0:def18

      mode Simplex of i,K -> finite Simplex of K means

      : Def18: ( card it ) = (i + 1) if ( - 1) <= i & i <= ( degree K)

      otherwise it is empty;

      existence

      proof

         A2:

        now

          reconsider S = ( {} K) as Simplex of K;

          assume

           A3: ( - 1) > i or i > ( degree K);

          take S;

          S is empty;

          hence thesis by A3;

        end;

        now

          assume

           A4: ( - 1) <= i & i <= ( degree K);

          then

          consider S be Simplex of K such that

           A5: ( card S) = (i + 1) by A1, Lm7;

          take S;

          reconsider i as Integer by A1;

          (( - 1) + 1) <= (i + 1) by A4, XXREAL_3: 35;

          then 0 <= (i + 1);

          then (i + 1) in NAT by INT_1: 3;

          then S is finite by A5;

          hence thesis by A4, A5;

        end;

        hence thesis by A2;

      end;

      correctness ;

    end

    registration

      let K;

      cluster -> empty for Simplex of ( - 1), K;

      coherence

      proof

        let S be Simplex of ( - 1), K;

        ( - 1) <= ( degree K) by Th23;

        

        then ( card S) = (( - 1) + 1) by Def18

        .= 0 ;

        hence thesis;

      end;

    end

    theorem :: SIMPLEX0:47

    for S be Simplex of i, K st S is non empty holds i is natural

    proof

      let S be Simplex of i, K;

      assume S is non empty;

      then ( - 1) <= i & i <> ( - 1) by Def18;

      then ( - 1) < i by XXREAL_0: 1;

      then i >= 0 by INT_1: 8;

      then i in NAT by INT_1: 3;

      hence thesis;

    end;

    theorem :: SIMPLEX0:48

    for S be finite Simplex of K holds S is Simplex of (( card S) - 1), K

    proof

      let S be finite Simplex of K;

      ( card S) <= (( degree K) + 1) by Th24;

      then (( card S) - 1) <= ((( degree K) + 1) - 1) by XXREAL_3: 37;

      then

       A1: (( card S) - 1) <= ( degree K) by XXREAL_3: 24;

      (( card S) - 1) >= ( 0 - 1) & ( card S) = ((( card S) - 1) + 1) by XREAL_1: 6;

      hence thesis by A1, Def18;

    end;

    theorem :: SIMPLEX0:49

    for K be non void subset-closed SimplicialComplexStr of D holds for S be non void SubSimplicialComplex of K holds for i be Integer, A be Simplex of i, S st A is non empty or i <= ( degree S) or ( degree S) = ( degree K) holds A is Simplex of i, K

    proof

      let K be non void subset-closed SimplicialComplexStr of D;

      let S be non void SubSimplicialComplex of K;

      let i be Integer, A be Simplex of i, S such that

       A1: A is non empty or i <= ( degree S) or ( degree S) = ( degree K);

      A in the topology of S & the topology of S c= the topology of K by Def13, PRE_TOPC:def 2;

      then A in the topology of K;

      then

      reconsider B = A as Simplex of K by PRE_TOPC:def 2;

      

       A2: ( degree S) <= ( degree K) by Th32;

      per cases by A1;

        suppose

         A3: A is non empty;

        then

         A4: ( - 1) <= i by Def18;

        

         A5: i <= ( degree S) by A3, Def18;

        ( - 1) <= i by A3, Def18;

        then

         A6: ( card B) = (i + 1) by A5, Def18;

        i <= ( degree K) by A2, A5, XXREAL_0: 2;

        hence thesis by A6, A4, Def18;

      end;

        suppose

         A7: i <= ( degree S);

        then

         A8: i <= ( degree K) by A2, XXREAL_0: 2;

        per cases ;

          suppose

           A9: ( - 1) <= i;

          then ( card B) = (i + 1) by A7, Def18;

          hence thesis by A8, A9, Def18;

        end;

          suppose

           A10: ( - 1) > i;

          then B is empty by Def18;

          hence thesis by A10, Def18;

        end;

      end;

        suppose

         A11: ( degree S) = ( degree K);

        per cases ;

          suppose

           A12: ( - 1) <= i & i <= ( degree S);

          then ( card B) = (i + 1) by Def18;

          hence thesis by A11, A12, Def18;

        end;

          suppose

           A13: ( - 1) > i or i > ( degree S);

          then B is empty by Def18;

          hence thesis by A11, A13, Def18;

        end;

      end;

    end;

    definition

      let K;

      let i be Real;

      let S be Simplex of i, K;

      :: SIMPLEX0:def19

      mode Face of S -> Simplex of ( max ((i - 1),( - 1))), K means

      : Def19: it c= S;

      existence

      proof

        per cases ;

          suppose i < 0 ;

          then (i - 1) < ( 0 - 1) by XREAL_1: 8;

          then

          reconsider F = the Simplex of ( - 1), K as Simplex of ( max ((i - 1),( - 1))), K by XXREAL_0:def 10;

          take F;

          thus thesis;

        end;

          suppose

           A3: i >= 0 ;

          then

           A4: ( card S) = (i + 1) by A1, A2, Def18;

          then S is non empty by A3;

          then

          consider x be object such that

           A5: x in S;

          reconsider I = i as Element of NAT by A1, A3, INT_1: 3;

          (i - 1) <= (( degree K) - 0 ) by A2, XXREAL_3: 37;

          then

           A6: (i - 1) <= ( degree K) by XXREAL_3: 4;

          reconsider Sx = (S \ {x}) as Simplex of K;

          

           A7: ( card Sx) = ((I - 1) + 1) by A4, A5, STIRL2_1: 55;

          

           A8: (i - 1) >= ( 0 - 1) by A3, XREAL_1: 6;

          then ( max ((i - 1),( - 1))) = (i - 1) by XXREAL_0:def 10;

          then

          reconsider Sx as Simplex of ( max ((i - 1),( - 1))), K by A6, A7, A8, Def18;

          take Sx;

          thus thesis by XBOOLE_1: 36;

        end;

      end;

    end

    theorem :: SIMPLEX0:50

    for S be Simplex of n, K st n <= ( degree K) holds X is Face of S iff ex x st x in S & (S \ {x}) = X

    proof

      let S be Simplex of n, K such that

       A1: n <= ( degree K);

      (n - 1) <= (n - 0 ) by XREAL_1: 6;

      then

       A2: (n - 1) <= ( degree K) by A1, XXREAL_0: 2;

      reconsider N = n as Integer;

      

       A3: (n - 1) >= ( 0 - 1) by XREAL_1: 6;

      then

       A4: ( max ((n - 1),( - 1))) = (n - 1) by XXREAL_0:def 10;

      

       A5: ( card S) = (N + 1) by A1, Def18;

      hereby

        assume X is Face of S;

        then

        reconsider f = X as Face of S;

        

         A6: f c= S by A1, Def19;

        ( card f) = ((n - 1) + 1) by A2, A3, A4, Def18;

        

        then ( card (S \ f)) = ((n + 1) - n) by A5, A6, CARD_2: 44

        .= 1;

        then

        consider x be object such that

         A7: (S \ f) = {x} by CARD_2: 42;

        reconsider x as set by TARSKI: 1;

        take x;

        x in {x} by TARSKI:def 1;

        hence x in S by A7, XBOOLE_0:def 5;

        

        thus (S \ {x}) = (f /\ S) by A7, XBOOLE_1: 48

        .= X by A6, XBOOLE_1: 28;

      end;

      given x such that

       A8: x in S and

       A9: (S \ {x}) = X;

      reconsider f = X as finite Simplex of K by A9;

      ( card f) = ((n - 1) + 1) by A5, A8, A9, STIRL2_1: 55;

      then

       A10: f is Simplex of (n - 1), K by A2, A3, Def18;

      X c= S by A9, XBOOLE_1: 36;

      hence thesis by A1, A4, A10, Def19;

    end;

    begin

    reserve P for Function;

    definition

      let X, KX, P;

      :: SIMPLEX0:def20

      func subdivision (P,KX) -> strict SimplicialComplexStr of X means

      : Def20: ( [#] it ) = ( [#] KX) & for A be Subset of it holds A is simplex-like iff ex S be c=-linear finite simplex-like Subset-Family of KX st A = (P .: S);

      existence

      proof

        defpred P[ set] means ex S be c=-linear finite simplex-like Subset-Family of KX st $1 = (P .: S);

        set SS = { A where A be Subset of KX : P[A] };

        SS c= ( bool the carrier of KX)

        proof

          let x be object;

          assume x in SS;

          then ex A be Subset of KX st x = A & P[A];

          hence thesis;

        end;

        then

        reconsider SS as Subset-Family of KX;

        set PP = TopStruct (# the carrier of KX, SS #);

        ( [#] PP) = ( [#] KX) & ( [#] KX) c= X by Def9;

        then

        reconsider PP as strict SimplicialComplexStr of X by Def9;

        take PP;

        thus ( [#] PP) = ( [#] KX);

        let A be Subset of PP;

        hereby

          assume A is simplex-like;

          then A in SS;

          then ex B be Subset of KX st B = A & P[B];

          hence P[A];

        end;

        assume P[A];

        then A in SS;

        hence thesis;

      end;

      uniqueness

      proof

        let P1,P2 be strict SimplicialComplexStr of X such that

         A1: ( [#] P1) = ( [#] KX) and

         A2: for A be Subset of P1 holds A is simplex-like iff ex S be c=-linear finite simplex-like Subset-Family of KX st A = (P .: S) and

         A3: ( [#] P2) = ( [#] KX) and

         A4: for A be Subset of P2 holds A is simplex-like iff ex S be c=-linear finite simplex-like Subset-Family of KX st A = (P .: S);

        now

          let x be object;

          hereby

            assume

             A5: x in the topology of P1;

            then

            reconsider A = x as Subset of P1;

            reconsider B = A as Subset of P2 by A1, A3;

            A is simplex-like by A5;

            then ex S be c=-linear finite simplex-like Subset-Family of KX st A = (P .: S) by A2;

            then B is simplex-like by A4;

            hence x in the topology of P2;

          end;

          assume

           A6: x in the topology of P2;

          then

          reconsider A = x as Subset of P2;

          reconsider B = A as Subset of P1 by A1, A3;

          A is simplex-like by A6;

          then ex S be c=-linear finite simplex-like Subset-Family of KX st A = (P .: S) by A4;

          then B is simplex-like by A2;

          hence x in the topology of P1;

        end;

        hence thesis by A1, A3, TARSKI: 2;

      end;

    end

    registration

      let X, KX, P;

      cluster ( subdivision (P,KX)) -> with_empty_element subset-closed finite-membered;

      coherence

      proof

        set PP = ( subdivision (P,KX));

        set S = the empty c=-linear simplex-like Subset-Family of KX;

        (P .: S) = ( {} KX);

        then ( {} PP) is simplex-like by Def20;

        then {} in the topology of PP;

        then the topology of PP is with_empty_element;

        hence PP is with_empty_element;

        thus PP is subset-closed

        proof

          let x, y;

          assume that

           A1: x in ( the_family_of PP) and

           A2: y c= x;

          reconsider X = x, Y = y as Subset of PP by A1, A2, XBOOLE_1: 1;

          X is simplex-like by A1;

          then

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

           A3: X = (P .: S) by Def20;

          set S1 = { A where A be Subset of KX : A in S & (P . A) in Y };

          S1 c= S

          proof

            let x be object;

            assume x in S1;

            then ex A be Subset of KX st A = x & A in S & (P . A) in Y;

            hence thesis;

          end;

          then

          reconsider S1 as c=-linear finite simplex-like Subset-Family of KX by TOPS_2: 11, XBOOLE_1: 1;

          

           A4: (P .: S1) c= Y

          proof

            let x be object;

            assume x in (P .: S1);

            then

            consider y be object such that y in ( dom P) and

             A5: y in S1 and

             A6: (P . y) = x by FUNCT_1:def 6;

            ex B be Subset of KX st y = B & B in S & (P . B) in Y by A5;

            hence thesis by A6;

          end;

          Y c= (P .: S1)

          proof

            let x be object;

            assume

             A7: x in Y;

            then

            consider y be object such that

             A8: y in ( dom P) and

             A9: y in S and

             A10: (P . y) = x by A2, A3, FUNCT_1:def 6;

            y in S1 by A7, A9, A10;

            hence thesis by A8, A10, FUNCT_1:def 6;

          end;

          then (P .: S1) = Y by A4;

          then Y is simplex-like by Def20;

          hence thesis;

        end;

        let x;

        assume

         A11: x in ( the_family_of PP);

        then

        reconsider A = x as Subset of PP;

        A is simplex-like by A11;

        then ex S be c=-linear finite simplex-like Subset-Family of KX st A = (P .: S) by Def20;

        hence thesis;

      end;

    end

    registration

      let X;

      let KX be void SimplicialComplexStr of X;

      let P;

      cluster ( subdivision (P,KX)) -> empty-membered;

      coherence

      proof

        set PP = ( subdivision (P,KX));

        assume PP is with_non-empty_element;

        then the topology of PP is with_non-empty_element;

        then

        consider x be non empty set such that

         A1: x in the topology of PP;

        reconsider A = x as Simplex of PP by A1, PRE_TOPC:def 2;

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

         A2: A = (P .: S) by Def20;

        A = (P .: (S /\ ( dom P))) by A2, RELAT_1: 112;

        then (S /\ ( dom P)) is non empty;

        then

        consider y be object such that

         A3: y in (S /\ ( dom P));

        

         A4: y in S by A3, XBOOLE_0:def 4;

        reconsider y as Subset of KX by A3;

        y is simplex-like by A4, TOPS_2:def 1;

        then y in the topology of KX;

        hence thesis by PENCIL_1:def 4;

      end;

    end

    theorem :: SIMPLEX0:51

    

     Th51: ( degree ( subdivision (P,KX))) <= (( degree KX) + 1)

    proof

      set PP = ( subdivision (P,KX));

      per cases ;

        suppose KX is void;

        then KX is empty-membered & ( degree PP) = ( - 1) by Th22;

        hence thesis;

      end;

        suppose

         A1: KX is non void non finite-degree;

        

         A2: ( degree PP) <= +infty & (( degree KX) + 0 ) <= (( degree KX) + 1) by XXREAL_0: 3, XXREAL_3: 36;

        (( degree KX) + 0 ) = ( degree KX) & ( degree KX) = +infty by A1, Def12, XXREAL_3: 4;

        hence thesis by A2, XXREAL_0: 2;

      end;

        suppose

         A3: KX is non void finite-degree;

        then

        reconsider d = ( degree KX) as Integer;

        reconsider d1 = (d + 1) as Nat by A3;

        for A be finite Subset of PP st A is simplex-like holds ( card A) <= ((d + 1) + 1)

        proof

          let A be finite Subset of PP;

          assume A is simplex-like;

          then

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

           A4: A = (P .: S) by Def20;

          set Sd = (S /\ ( dom P));

          A = (P .: (S /\ ( dom P))) by A4, RELAT_1: 112;

          then ( Segm ( card A)) c= ( Segm ( card Sd)) by CARD_1: 67;

          then

           A5: ( card A) <= ( card Sd) by NAT_1: 39;

          (Sd \ { {} }) c= S by XBOOLE_1: 18, XBOOLE_1: 36;

          then

          reconsider SP = (Sd \ { {} }) as c=-linear finite simplex-like Subset-Family of KX by TOPS_2: 11;

          (SP \/ { {} }) = (Sd \/ { {} }) by XBOOLE_1: 39;

          then

           A6: ( card { {} }) = 1 & ( card Sd) <= ( card (SP \/ { {} })) by CARD_1: 30, NAT_1: 43, XBOOLE_1: 7;

          ( card (SP \/ { {} })) <= (( card SP) + ( card { {} })) by CARD_2: 43;

          then

           A7: ( card Sd) <= (( card SP) + 1) by A6, XXREAL_0: 2;

          per cases ;

            suppose

             A8: SP is empty;

            ( 0 + 1) <= (d1 + 1) by XREAL_1: 6;

            then ( card Sd) <= (d1 + 1) by A6, A8, XXREAL_0: 2;

            hence thesis by A5, XXREAL_0: 2;

          end;

            suppose

             A9: SP is non empty;

            reconsider uSP = ( union SP) as Subset of KX;

            ( union SP) in SP by A9, Th9;

            then

             A10: uSP is simplex-like by TOPS_2:def 1;

             not {} in SP by ZFMISC_1: 56;

            then SP is with_non-empty_elements;

            then

             A11: ( card SP) c= ( card ( union SP)) by Th10;

            reconsider uSP as finite Subset of KX by A3;

            ( card uSP) <= d1 by A3, A10, Th25;

            then ( Segm ( card uSP)) c= ( Segm d1) by NAT_1: 39;

            then ( Segm ( card SP)) c= ( Segm d1) by A11;

            then ( card SP) <= d1 by NAT_1: 39;

            then (( card SP) + 1) <= (d1 + 1) by XREAL_1: 6;

            then ( card Sd) <= (d1 + 1) by A7, XXREAL_0: 2;

            hence thesis by A5, XXREAL_0: 2;

          end;

        end;

        hence thesis by Th25;

      end;

    end;

    theorem :: SIMPLEX0:52

    

     Th52: ( dom P) is with_non-empty_elements implies ( degree ( subdivision (P,KX))) <= ( degree KX)

    proof

      assume

       A1: ( dom P) is with_non-empty_elements;

      set PP = ( subdivision (P,KX));

      per cases ;

        suppose

         A2: KX is non finite-degree;

        KX is non void

        proof

          assume KX is void;

          then KX is empty-membered;

          hence thesis by A2;

        end;

        then ( degree KX) = +infty by A2, Def12;

        hence thesis by XXREAL_0: 3;

      end;

        suppose

         A3: KX is finite-degree;

        then

        reconsider d = ( degree KX) as Integer;

        reconsider d1 = (d + 1) as Nat by A3;

        for A be finite Subset of PP st A is simplex-like holds ( card A) <= (d + 1)

        proof

          let A be finite Subset of PP;

          assume A is simplex-like;

          then

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

           A4: A = (P .: S) by Def20;

          

           A5: A = (P .: (S /\ ( dom P))) by A4, RELAT_1: 112;

          per cases ;

            suppose (S /\ ( dom P)) is empty;

            then 0 <= d1 & A = {} by A5;

            hence thesis;

          end;

            suppose

             A6: (S /\ ( dom P)) is non empty;

            reconsider uSP = ( union (S /\ ( dom P))) as Subset of KX;

            

             A7: (S /\ ( dom P)) c= S by XBOOLE_1: 17;

            then ( union (S /\ ( dom P))) in (S /\ ( dom P)) by A6, Th9;

            then ( union (S /\ ( dom P))) in S by XBOOLE_0:def 4;

            then

             A8: uSP is simplex-like by TOPS_2:def 1;

            then

             A9: uSP in the topology of KX;

            ( the_family_of KX) is finite-membered by A3, MATROID0:def 6;

            then

            reconsider uSP as finite Subset of KX by A9;

            KX is non void by A9, PENCIL_1:def 4;

            then ( card uSP) <= (d + 1) by A8, Th25;

            then

             A10: ( Segm ( card uSP)) c= ( Segm d1) by NAT_1: 39;

            ( card (S /\ ( dom P))) c= ( card ( union (S /\ ( dom P)))) by A1, A7, Th10;

            then

             A11: ( card (S /\ ( dom P))) c= d1 by A10;

            ( card A) c= ( card (S /\ ( dom P))) by A5, CARD_1: 67;

            then ( Segm ( card A)) c= ( Segm d1) by A11;

            hence thesis by NAT_1: 39;

          end;

        end;

        hence thesis by Th25;

      end;

    end;

    registration

      let X;

      let KX be finite-degree SimplicialComplexStr of X;

      let P;

      cluster ( subdivision (P,KX)) -> finite-degree;

      coherence

      proof

        assume ( subdivision (P,KX)) is non finite-degree;

        then (( degree KX) + 1) in REAL & ( degree ( subdivision (P,KX))) = +infty by Def12, XREAL_0:def 1;

        hence thesis by Th51, XXREAL_0: 9;

      end;

    end

    registration

      let X;

      let KX be finite-vertices SimplicialComplexStr of X;

      let P;

      cluster ( subdivision (P,KX)) -> finite-vertices;

      coherence

      proof

        reconsider V = ( Vertices KX) as finite Subset of KX by Def5;

        set PP = ( subdivision (P,KX));

        set TOP = the topology of PP;

        defpred F[ object, object] means ex D2 be set st D2 = $2 & (P .: D2) = $1;

        ( bool V) = ( bool ( union the topology of KX)) by Lm5;

        then

         A1: the topology of KX c= ( bool V) by ZFMISC_1: 82;

        

         A2: for x be object st x in TOP holds ex y be object st y in ( bool ( bool V)) & F[x, y]

        proof

          let x be object such that

           A3: x in TOP;

          reconsider X = x as Subset of PP by A3;

          X is simplex-like by A3;

          then

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

           A4: X = (P .: S) by Def20;

          take S;

          S c= the topology of KX

          proof

            let y be object such that

             A5: y in S;

            reconsider Y = y as Subset of KX by A5;

            Y is simplex-like by A5, TOPS_2:def 1;

            hence thesis;

          end;

          then S c= ( bool V) by A1;

          hence thesis by A4;

        end;

        consider f be Function of TOP, ( bool ( bool V)) such that

         A6: for x be object st x in TOP holds F[x, (f . x)] from FUNCT_2:sch 1( A2);

        now

          let x1,x2 be object such that

           A7: x1 in ( dom f) and

           A8: x2 in ( dom f) & (f . x1) = (f . x2);

          

           A9: F[x2, (f . x2)] by A6, A8;

           F[x1, (f . x1)] by A6, A7;

          

          hence x1 = (P .: (f . x1))

          .= x2 by A8, A9;

        end;

        then

         A10: f is one-to-one by FUNCT_1:def 4;

        ( dom f) = TOP & ( rng f) c= ( bool ( bool V)) by FUNCT_2:def 1;

        then ( card TOP) c= ( card ( bool ( bool V))) by A10, CARD_1: 10;

        then TOP is finite;

        hence thesis by Th20;

      end;

    end

    theorem :: SIMPLEX0:53

    for KX be subset-closed SimplicialComplexStr of X holds for P st ( dom P) is with_non-empty_elements & for n st n <= ( degree KX) holds ex S be Subset of KX st S is simplex-like & ( card S) = (n + 1) & ( BOOL S) c= ( dom P) & (P .: ( BOOL S)) is Subset of KX & (P | ( BOOL S)) is one-to-one holds ( degree ( subdivision (P,KX))) = ( degree KX)

    proof

      let K be subset-closed SimplicialComplexStr of X;

      let P be Function such that

       A1: ( dom P) is with_non-empty_elements and

       A2: for n st n <= ( degree K) holds ex S be Subset of K st S is simplex-like & ( card S) = (n + 1) & ( BOOL S) c= ( dom P) & (P .: ( BOOL S)) is Subset of K & (P | ( BOOL S)) is one-to-one;

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

      

       A3: ( degree PP) <= ( degree K) by A1, Th52;

      

       A4: for n st n <= ( degree K) holds ex S be Simplex of PP st ( card S) = (n + 1)

      proof

        let n;

        

         A5: ( [#] K) = ( [#] PP) by Def20;

        assume n <= ( degree K);

        then

        consider A be Subset of K such that

         A6: A is simplex-like and

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

         A8: ( BOOL A) c= ( dom P) and

         A9: (P .: ( BOOL A)) is Subset of K and

         A10: (P | ( BOOL A)) is one-to-one by A2;

        

         A11: ( dom (P | ( BOOL A))) = ( BOOL A) by A8, RELAT_1: 62;

        A is non empty by A7;

        then

        consider S be Subset-Family of A such that

         A12: S is with_non-empty_elements c=-linear and A in S and

         A13: ( card A) = ( card S) and for Z st Z in S & ( card Z) <> 1 holds ex x st x in Z & (Z \ {x}) in S by Th12;

        ( bool A) c= ( bool the carrier of K) by ZFMISC_1: 67;

        then

        reconsider SS = S as Subset-Family of K by XBOOLE_1: 1;

        

         A14: S c= ( BOOL A)

        proof

          let x be object;

          assume x in S;

          then x in (( bool A) \ { {} }) by A12, ZFMISC_1: 56;

          hence thesis by ORDERS_1:def 3;

        end;

        then (P .: S) c= (P .: ( BOOL A)) by RELAT_1: 123;

        then

        reconsider PS = (P .: SS) as Subset of PP by A5, A9, XBOOLE_1: 1;

        

         A15: A in ( the_family_of K) by A6;

        SS is simplex-like

        proof

          let B be Subset of K;

          assume B in SS;

          then B in ( the_family_of K) by A15, CLASSES1:def 1;

          hence thesis;

        end;

        then SS is c=-linear finite simplex-like Subset-Family of K by A7, A12, A13;

        then

        reconsider PS as Simplex of PP by Def20;

        (P .: S) = ((P | ( BOOL A)) .: S) by A14, RELAT_1: 129;

        then ( card PS) = (n + 1) by A7, A10, A11, A13, A14, COMBGRAS: 4;

        hence thesis;

      end;

      per cases ;

        suppose

         A16: K is empty-membered;

        

         A17: ( degree PP) >= ( - 1) by Th23;

        ( degree K) = ( - 1) by A16, Th22;

        hence thesis by A3, A17, XXREAL_0: 1;

      end;

        suppose

         A18: K is with_non-empty_element finite-degree;

        then

        reconsider d = ( degree K), dPP = ( degree PP) as Integer;

        

         A19: ( - 1) <= d by Th23;

        d <> ( - 1) by A18, Th22;

        then ( - 1) < d by A19, XXREAL_0: 1;

        then 0 <= d by INT_1: 8;

        then

        reconsider d as Element of NAT by INT_1: 3;

        ex S be Simplex of PP st ( card S) = (d + 1) by A4;

        then (dPP + 1) >= (d + 1) by A18, Def12;

        then dPP >= d by XREAL_1: 6;

        hence thesis by A3, XXREAL_0: 1;

      end;

        suppose K is non void non finite-degree;

        then

         A20: ( degree K) = +infty by Def12;

        PP is non finite-degree

        proof

          assume

           A21: PP is finite-degree;

          then

          reconsider d = (( degree PP) + 1) as Nat by TARSKI: 1;

          consider S be Subset of PP such that

           A22: S is simplex-like and

           A23: ( card S) = d by A21, Def12;

          reconsider S as finite Subset of PP by A22;

          ex S1 be Simplex of PP st ( card S1) = (( card S) + 1) by A4, A20, XXREAL_0: 3;

          then (d + 1) <= d by A21, A23, Def12;

          hence contradiction by NAT_1: 13;

        end;

        hence thesis by A20, Def12;

      end;

    end;

    theorem :: SIMPLEX0:54

    

     Th54: Y c= Z implies ( subdivision ((P | Y),KX)) is SubSimplicialComplex of ( subdivision ((P | Z),KX))

    proof

      set PY = ( subdivision ((P | Y),KX));

      set PZ = ( subdivision ((P | Z),KX));

      

       A1: ( dom (P | Z)) = (Z /\ ( dom P)) by RELAT_1: 61;

      assume

       A2: Y c= Z;

      then (Y /\ Z) = Y by XBOOLE_1: 28;

      

      then

       A3: ( dom (P | Y)) = ((Z /\ Y) /\ ( dom P)) by RELAT_1: 61

      .= (Y /\ ( dom (P | Z))) by A1, XBOOLE_1: 16;

      

       A4: ( [#] PY) = ( [#] KX) by Def20;

      hence ( [#] PY) c= ( [#] PZ) by Def20;

      let x be object;

      assume x in the topology of PY;

      then

      reconsider A = x as Simplex of PY by PRE_TOPC:def 2;

      ( [#] PZ) = ( [#] KX) by Def20;

      then

      reconsider B = A as Subset of PZ by A4;

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

       A5: A = ((P | Y) .: S) by Def20;

      (S /\ Y) c= S by XBOOLE_1: 17;

      then

      reconsider SY = (S /\ Y) as c=-linear finite simplex-like Subset-Family of KX by TOPS_2: 11;

      

       A6: ( dom (P | Y)) c= Y & (( dom (P | Y)) /\ S) c= ( dom (P | Y)) by RELAT_1: 58, XBOOLE_1: 17;

      then

       A7: (( dom (P | Y)) /\ S) c= Y;

      B = ((P | Y) .: (( dom (P | Y)) /\ S)) by A5, RELAT_1: 112

      .= (P .: (( dom (P | Y)) /\ S)) by A6, RELAT_1: 129, XBOOLE_1: 1

      .= ((P | Z) .: (( dom (P | Y)) /\ S)) by A2, A7, RELAT_1: 129, XBOOLE_1: 1

      .= ((P | Z) .: (( dom (P | Z)) /\ SY)) by A3, XBOOLE_1: 16

      .= ((P | Z) .: SY) by RELAT_1: 112;

      then B is simplex-like by Def20;

      hence thesis;

    end;

    theorem :: SIMPLEX0:55

    (( dom P) /\ the topology of KX) c= Y implies ( subdivision ((P | Y),KX)) = ( subdivision (P,KX))

    proof

      set PX = ( subdivision ((P | Y),KX));

      set PP = ( subdivision (P,KX));

      

       A1: ((P | Y) | ( dom (P | Y))) = (P | ( dom (P | Y))) by RELAT_1: 58, RELAT_1: 74;

      

       A2: ( [#] PX) = ( [#] KX) & ( [#] PP) = ( [#] KX) by Def20;

      assume

       A3: (( dom P) /\ the topology of KX) c= Y;

      

       A4: the topology of PP c= the topology of PX

      proof

        let x be object;

        assume x in the topology of PP;

        then

        reconsider A = x as Simplex of PP by PRE_TOPC:def 2;

        reconsider B = A as Subset of PX by A2;

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

         A5: A = (P .: S) by Def20;

        

         A6: (S /\ ( dom P)) c= Y

        proof

          let x be object;

          assume

           A7: x in (S /\ ( dom P));

          then

          reconsider A = x as Subset of KX;

          x in S by A7, XBOOLE_0:def 4;

          then A is simplex-like by TOPS_2:def 1;

          then

           A8: A in the topology of KX;

          x in ( dom P) by A7, XBOOLE_0:def 4;

          then A in (the topology of KX /\ ( dom P)) by A8, XBOOLE_0:def 4;

          hence thesis by A3;

        end;

        then

         A9: ((S /\ ( dom P)) /\ Y) = (S /\ ( dom P)) by XBOOLE_1: 28;

        B = (P .: (S /\ ( dom P))) by A5, RELAT_1: 112

        .= ((P | Y) .: ((S /\ ( dom P)) /\ Y)) by A6, A9, RELAT_1: 129

        .= ((P | Y) .: (S /\ (( dom P) /\ Y))) by XBOOLE_1: 16

        .= ((P | Y) .: (S /\ ( dom (P | Y)))) by RELAT_1: 61

        .= ((P | Y) .: S) by RELAT_1: 112;

        then B is simplex-like by Def20;

        hence thesis;

      end;

      (P | ( dom P)) = P & (P | Y) = ((P | Y) | ( dom (P | Y)));

      then PX is SubSimplicialComplex of PP by A1, Th54, RELAT_1: 60;

      then the topology of PX c= the topology of PP by Def13;

      hence thesis by A2, A4, XBOOLE_0:def 10;

    end;

    theorem :: SIMPLEX0:56

    

     Th56: Y c= Z implies ( subdivision ((Y |` P),KX)) is SubSimplicialComplex of ( subdivision ((Z |` P),KX))

    proof

      assume

       A1: Y c= Z;

      set PZ = ( subdivision ((Z |` P),KX));

      set PY = ( subdivision ((Y |` P),KX));

      

       A2: ( [#] PY) = ( [#] KX) by Def20;

      hence ( [#] PY) c= ( [#] PZ) by Def20;

      let x be object;

      assume x in the topology of PY;

      then

      reconsider A = x as Simplex of PY by PRE_TOPC:def 2;

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

       A3: A = ((Y |` P) .: S) by Def20;

      (S /\ ( dom (Y |` P))) c= S by XBOOLE_1: 17;

      then

      reconsider Sd = (S /\ ( dom (Y |` P))) as c=-linear finite simplex-like Subset-Family of KX by TOPS_2: 11;

      (Y |` (Z |` P)) = (Y |` P) by A1, RELAT_1: 99;

      then

       A4: ((Y |` P) .: Sd) c= ((Z |` P) .: Sd) by RELAT_1: 86, RELAT_1: 124;

      ( [#] PZ) = ( [#] KX) by Def20;

      then

      reconsider A as Subset of PZ by A2;

      

       A5: ((Z |` P) .: Sd) c= ((Y |` P) .: Sd)

      proof

        let y be object;

        assume y in ((Z |` P) .: Sd);

        then

        consider x be object such that

         A6: x in ( dom (Z |` P)) and

         A7: x in Sd and

         A8: ((Z |` P) . x) = y by FUNCT_1:def 6;

        

         A9: x in ( dom (Y |` P)) by A7, XBOOLE_0:def 4;

        (P . x) = y by A6, A8, FUNCT_1: 53;

        then ((Y |` P) . x) = y by A9, FUNCT_1: 53;

        hence thesis by A7, A9, FUNCT_1:def 6;

      end;

      A = ((Y |` P) .: Sd) by A3, RELAT_1: 112;

      then A = ((Z |` P) .: Sd) by A4, A5;

      then A is simplex-like by Def20;

      hence thesis;

    end;

    theorem :: SIMPLEX0:57

    (P .: the topology of KX) c= Y implies ( subdivision ((Y |` P),KX)) = ( subdivision (P,KX))

    proof

      set PK = ( subdivision (P,KX));

      P = (( rng P) |` P) & (Y |` (( rng P) |` P)) = ((Y /\ ( rng P)) |` P) by RELAT_1: 96;

      then

      reconsider PY = ( subdivision ((Y |` P),KX)) as SubSimplicialComplex of PK by Th56, XBOOLE_1: 17;

      

       A1: ( [#] PY) = ( [#] KX) & ( [#] PK) = ( [#] KX) by Def20;

      assume

       A2: (P .: the topology of KX) c= Y;

      

       A3: the topology of PK c= the topology of PY

      proof

        let x be object;

        assume x in the topology of PK;

        then

        reconsider A = x as Simplex of PK by PRE_TOPC:def 2;

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

         A4: A = (P .: S) by Def20;

        reconsider A as Subset of PY by A1;

        S c= the topology of KX

        proof

          let y be object such that

           A5: y in S;

          reconsider y as Subset of KX by A5;

          y is simplex-like by A5, TOPS_2:def 1;

          hence thesis;

        end;

        then A c= (P .: the topology of KX) by A4, RELAT_1: 123;

        then (A /\ Y) = A by A2, XBOOLE_1: 1, XBOOLE_1: 28;

        then A = ((Y |` P) .: S) by A4, FUNCT_1: 67;

        then A is simplex-like by Def20;

        hence thesis;

      end;

      the topology of PY c= the topology of PK by Def13;

      hence thesis by A1, A3, XBOOLE_0:def 10;

    end;

    theorem :: SIMPLEX0:58

    

     Th58: ( subdivision (P,SX)) is SubSimplicialComplex of ( subdivision (P,KX))

    proof

      set PS = ( subdivision (P,SX));

      set PK = ( subdivision (P,KX));

      

       A1: ( [#] SX) c= ( [#] KX) by Def13;

      

       A2: ( [#] PK) = ( [#] KX) by Def20;

      hence ( [#] PS) c= ( [#] PK) by A1, Def20;

      let x be object;

      assume x in the topology of PS;

      then

      reconsider A = x as Simplex of PS by PRE_TOPC:def 2;

      ( [#] PS) = ( [#] SX) by Def20;

      then

      reconsider B = A as Subset of PK by A1, A2, XBOOLE_1: 1;

      consider SS be c=-linear finite simplex-like Subset-Family of SX such that

       A3: A = (P .: SS) by Def20;

      ( bool ( [#] SX)) c= ( bool ( [#] KX)) by A1, ZFMISC_1: 67;

      then

      reconsider SK = SS as c=-linear finite Subset-Family of KX by XBOOLE_1: 1;

      SK is simplex-like

      proof

        let C be Subset of KX;

        assume

         A4: C in SK;

        then

        reconsider c = C as Subset of SX;

        c is simplex-like by A4, TOPS_2:def 1;

        then

         A5: c in the topology of SX;

        the topology of SX c= the topology of KX by Def13;

        hence thesis by A5;

      end;

      then B is simplex-like by A3, Def20;

      hence thesis;

    end;

    theorem :: SIMPLEX0:59

    for A be Subset of ( subdivision (P,KX)) st ( dom P) c= the topology of SX & A = ( [#] SX) holds ( subdivision (P,SX)) = (( subdivision (P,KX)) | A)

    proof

      set PK = ( subdivision (P,KX));

      reconsider PS = ( subdivision (P,SX)) as strict SubSimplicialComplex of PK by Th58;

      let A be Subset of ( subdivision (P,KX)) such that

       A1: ( dom P) c= the topology of SX and

       A2: A = ( [#] SX);

      now

        let a be Subset of PS;

        assume a in the topology of PK;

        then

        reconsider b = a as Simplex of PK by PRE_TOPC:def 2;

        consider SS be c=-linear finite simplex-like Subset-Family of KX such that

         A3: b = (P .: SS) by Def20;

        (SS /\ ( dom P)) c= ( dom P) by XBOOLE_1: 17;

        then

         A4: (SS /\ ( dom P)) c= the topology of SX by A1;

        (SS /\ ( dom P)) c= SS by XBOOLE_1: 17;

        then

        reconsider Sd = (SS /\ ( dom P)) as c=-linear finite Subset-Family of SX by A4, XBOOLE_1: 1;

        

         A5: Sd is simplex-like

        proof

          let B be Subset of SX;

          assume B in Sd;

          then B in ( dom P) by XBOOLE_0:def 4;

          hence thesis by A1;

        end;

        (P .: SS) = (P .: Sd) by RELAT_1: 112;

        hence a is simplex-like by A3, A5, Def20;

      end;

      then

       A6: PS is maximal;

      ( [#] PS) = ( [#] SX) by Def20;

      hence thesis by A2, A6, Def16;

    end;

    theorem :: SIMPLEX0:60

    

     Th60: for K1,K2 be SimplicialComplexStr of X st the TopStruct of K1 = the TopStruct of K2 holds ( subdivision (P,K1)) = ( subdivision (P,K2))

    proof

      let K1,K2 be SimplicialComplexStr of X such that

       A1: the TopStruct of K1 = the TopStruct of K2;

      set P1 = ( subdivision (P,K1)), P2 = ( subdivision (P,K2));

      

       A2: ( [#] K1) = ( [#] P1) & ( [#] K2) = ( [#] P2) by Def20;

      

       A3: the topology of P1 c= the topology of P2

      proof

        let x be object;

        assume

         A4: x in the topology of P1;

        then

        reconsider A = x as Subset of P1;

        reconsider A1 = A as Subset of P2 by A1, A2;

        A is simplex-like by A4;

        then

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

         A5: A = (P .: S) by Def20;

        reconsider S1 = S as Subset-Family of K2 by A1;

        S c= the topology of K1 by Th14;

        then S1 is simplex-like by A1, Th14;

        then A1 is simplex-like by A5, Def20;

        hence thesis;

      end;

      the topology of P2 c= the topology of P1

      proof

        let x be object;

        assume

         A6: x in the topology of P2;

        then

        reconsider A = x as Subset of P2;

        reconsider A1 = A as Subset of P1 by A1, A2;

        A is simplex-like by A6;

        then

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

         A7: A = (P .: S) by Def20;

        reconsider S1 = S as Subset-Family of K1 by A1;

        S c= the topology of K2 by Th14;

        then S1 is simplex-like by A1, Th14;

        then A1 is simplex-like by A7, Def20;

        hence thesis;

      end;

      hence thesis by A1, A2, A3, XBOOLE_0:def 10;

    end;

    definition

      let X, KX, P, n;

      :: SIMPLEX0:def21

      func subdivision (n,P,KX) -> SimplicialComplexStr of X means

      : Def21: ex F be Function st (F . 0 ) = KX & (F . n) = it & ( dom F) = NAT & for k holds for KX1 be SimplicialComplexStr of X st KX1 = (F . k) holds (F . (k + 1)) = ( subdivision (P,KX1));

      existence

      proof

        defpred F[ object, object] means for SX be SimplicialComplexStr of X st the topology of SX = $1 & ( [#] SX) = ( [#] KX) holds the topology of ( subdivision (P,SX)) = $2;

        set BBK = ( bool ( bool ( [#] KX)));

        

         A1: for x be object st x in BBK holds ex y be object st y in BBK & F[x, y]

        proof

          let x be object;

          assume

           A2: x in BBK;

          per cases ;

            suppose ex SX be SimplicialComplexStr of X st the topology of SX = x & ( [#] SX) = ( [#] KX);

            then

            consider SX be SimplicialComplexStr of X such that

             A3: the topology of SX = x and

             A4: ( [#] SX) = ( [#] KX);

            take T = the topology of ( subdivision (P,SX));

            ( [#] ( subdivision (P,SX))) = ( [#] SX) by Def20;

            hence T in BBK by A4;

            let SX1 be SimplicialComplexStr of X such that

             A5: the topology of SX1 = x & ( [#] SX1) = ( [#] KX);

             the TopStruct of SX = the TopStruct of SX1 by A3, A4, A5;

            hence thesis by Th60;

          end;

            suppose

             A6: for SX be SimplicialComplexStr of X holds the topology of SX <> x or ( [#] SX) <> ( [#] KX);

            take x;

            thus thesis by A2, A6;

          end;

        end;

        consider f be Function of BBK, BBK such that

         A7: for x be object st x in BBK holds F[x, (f . x)] from FUNCT_2:sch 1( A1);

        deffunc G( set, set) = (f . $2);

        consider g be Function such that

         A8: ( dom g) = NAT & (g . 0 ) = the topology of KX & for n be Nat holds (g . (n + 1)) = G(n,.) from NAT_1:sch 11;

        defpred P[ Nat] means (ex SX be SimplicialComplexStr of X st the topology of SX = (g . $1) & ( [#] SX) = ( [#] KX) & ($1 > 0 implies SX is strict)) & for SX be SimplicialComplexStr of X st the topology of SX = (g . $1) & ( [#] SX) = ( [#] KX) holds (g . ($1 + 1)) = the topology of ( subdivision (P,SX));

        (g . ( 0 + 1)) = (f . the topology of KX) by A8;

        then

         A9: (g . 1) = the topology of ( subdivision (P,KX)) by A7;

        

         A10: P[ 0 qua Nat]

        proof

          thus ex SX be SimplicialComplexStr of X st the topology of SX = (g . 0 ) & ( [#] SX) = ( [#] KX) & ( 0 > 0 implies SX is strict) by A8;

          let SX be SimplicialComplexStr of X;

          assume the topology of SX = (g . 0 ) & ( [#] SX) = ( [#] KX);

          then the TopStruct of SX = the TopStruct of KX by A8;

          hence thesis by A9, Th60;

        end;

        defpred H[ object, object] means for k be Nat st k = $1 holds (k = 0 implies $2 = KX) & (k > 0 implies for SF be Subset-Family of KX st SF = (g . k) holds $2 = TopStruct (# the carrier of KX, SF #));

        

         A11: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          set k1 = (k + 1);

          given SX be SimplicialComplexStr of X such that

           A12: the topology of SX = (g . k) and

           A13: ( [#] SX) = ( [#] KX) and k > 0 implies SX is strict;

          assume for SX be SimplicialComplexStr of X st the topology of SX = (g . k) & ( [#] SX) = ( [#] KX) holds (g . k1) = the topology of ( subdivision (P,SX));

          then

           A14: (g . k1) = the topology of ( subdivision (P,SX)) by A12, A13;

          ( [#] ( subdivision (P,SX))) = ( [#] KX) by A13, Def20;

          hence ex SX be SimplicialComplexStr of X st the topology of SX = (g . k1) & ( [#] SX) = ( [#] KX) & (k1 > 0 implies SX is strict) by A14;

          let S1 be SimplicialComplexStr of X;

          assume

           A15: the topology of S1 = (g . k1) & ( [#] S1) = ( [#] KX);

          (g . (k1 + 1)) = (f . (g . k1)) by A8;

          hence thesis by A7, A15;

        end;

        

         A16: for k be Nat holds P[k] from NAT_1:sch 2( A10, A11);

        

         A17: for x be object st x in NAT holds ex y be object st H[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider m = x as Nat;

          per cases ;

            suppose

             A18: m = 0 ;

            take KX;

            thus thesis by A18;

          end;

            suppose

             A19: m > 0 ;

            consider K1 be SimplicialComplexStr of X such that

             A20: the topology of K1 = (g . m) and

             A21: ( [#] K1) = ( [#] KX) and m > 0 implies K1 is strict by A16;

            reconsider TOP = the topology of K1 as Subset-Family of KX by A21;

            take TopStruct (# the carrier of KX, TOP #);

            thus thesis by A19, A20;

          end;

        end;

        consider h be Function such that

         A22: ( dom h) = NAT & for x be object st x in NAT holds H[x, (h . x)] from CLASSES1:sch 1( A17);

        

         A23: (h . 0 ) = KX by A22;

        

         A24: for k be Nat holds for K1 be SimplicialComplexStr of X st (h . k) = K1 holds (h . (k + 1)) = ( subdivision (P,K1))

        proof

          let k be Nat;

          let KK be SimplicialComplexStr of X such that

           A25: (h . k) = KK;

           P[(k + 1)] by A16;

          then

          consider K1 be SimplicialComplexStr of X such that

           A26: the topology of K1 = (g . (k + 1)) and

           A27: ( [#] K1) = ( [#] KX);

          reconsider TOP1 = the topology of K1 as Subset-Family of KX by A27;

          

           A28: k in NAT by ORDINAL1:def 12;

           P[k] by A16;

          then

          consider K2 be SimplicialComplexStr of X such that

           A29: the topology of K2 = (g . k) and

           A30: ( [#] K2) = ( [#] KX);

          reconsider TOP2 = the topology of K2 as Subset-Family of KX by A30;

          

           A31: ( [#] ( subdivision (P,KK))) = ( [#] KK) by Def20;

          per cases ;

            suppose

             A32: k = 0 ;

            then TOP1 = the topology of ( subdivision (P,KK)) by A8, A10, A23, A25, A26;

            hence thesis by A22, A23, A25, A26, A31, A32;

          end;

            suppose k > 0 ;

            then

             A33: KK = TopStruct (# the carrier of KX, TOP2 #) by A22, A25, A28, A29;

            then ( [#] KK) = ( [#] KX);

            then (g . (k + 1)) = the topology of ( subdivision (P,KK)) by A16, A29, A33;

            hence thesis by A22, A31, A33;

          end;

        end;

        per cases ;

          suppose

           A34: n = 0 ;

          take KX;

          thus thesis by A22, A23, A24, A34;

        end;

          suppose

           A35: n > 0 ;

          consider K1 be SimplicialComplexStr of X such that

           A36: the topology of K1 = (g . n) and

           A37: ( [#] K1) = ( [#] KX) and

           A38: n > 0 implies K1 is strict by A16;

          reconsider K1 as strict SimplicialComplexStr of X by A35, A38;

          take K1, h;

          thus (h . 0 ) = KX by A22;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A22, A24, A35, A36, A37;

        end;

      end;

      uniqueness

      proof

        let P1,P2 be SimplicialComplexStr of X;

        given F1 be Function such that

         A39: (F1 . 0 ) = KX and

         A40: (F1 . n) = P1 and ( dom F1) = NAT and

         A41: for k holds for KX1 be SimplicialComplexStr of X st KX1 = (F1 . k) holds (F1 . (k + 1)) = ( subdivision (P,KX1));

        given F2 be Function such that

         A42: (F2 . 0 ) = KX and

         A43: (F2 . n) = P2 and ( dom F2) = NAT and

         A44: for k holds for KX1 be SimplicialComplexStr of X st KX1 = (F2 . k) holds (F2 . (k + 1)) = ( subdivision (P,KX1));

        defpred P[ Nat] means (F1 . $1) = (F2 . $1) & ex KX1 be SimplicialComplexStr of X st KX1 = (F1 . $1);

        

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

        proof

          let k such that

           A46: P[k];

          consider KX1 be SimplicialComplexStr of X such that

           A47: KX1 = (F1 . k) by A46;

          (F1 . (k + 1)) = ( subdivision (P,KX1)) by A41, A47;

          hence thesis by A44, A46, A47;

        end;

        

         A48: P[ 0 qua Nat] by A39, A42;

        for k holds P[k] from NAT_1:sch 2( A48, A45);

        hence thesis by A40, A43;

      end;

    end

    theorem :: SIMPLEX0:61

    

     Th61: ( subdivision ( 0 ,P,KX)) = KX

    proof

      ex F be Function st (F . 0 ) = KX & (F . 0 ) = ( subdivision ( 0 ,P,KX)) & ( dom F) = NAT & for k holds for KX1 be SimplicialComplexStr of X st KX1 = (F . k) holds (F . (k + 1)) = ( subdivision (P,KX1)) by Def21;

      hence thesis;

    end;

    theorem :: SIMPLEX0:62

    

     Th62: ( subdivision (1,P,KX)) = ( subdivision (P,KX))

    proof

      consider F be Function such that

       A1: (F . 0 ) = KX and

       A2: (F . 1) = ( subdivision (1,P,KX)) and ( dom F) = NAT and

       A3: for k holds for KX1 be SimplicialComplexStr of X st KX1 = (F . k) holds (F . (k + 1)) = ( subdivision (P,KX1)) by Def21;

      (F . ( 0 + 1)) = ( subdivision (P,KX)) by A1, A3;

      hence thesis by A2;

    end;

    theorem :: SIMPLEX0:63

    

     Th63: for n,k be Element of NAT holds ( subdivision ((n + k),P,KX)) = ( subdivision (n,P,( subdivision (k,P,KX))))

    proof

      let n,k be Element of NAT ;

      consider Fn be Function such that

       A1: (Fn . 0 ) = ( subdivision (k,P,KX)) and

       A2: (Fn . n) = ( subdivision (n,P,( subdivision (k,P,KX)))) and ( dom Fn) = NAT and

       A3: for m be Nat holds for KX1 be SimplicialComplexStr of X st KX1 = (Fn . m) holds (Fn . (m + 1)) = ( subdivision (P,KX1)) by Def21;

      consider Fnm be Function such that

       A4: (Fnm . 0 ) = KX and

       A5: (Fnm . (n + k)) = ( subdivision ((n + k),P,KX)) and ( dom Fnm) = NAT and

       A6: for m be Nat holds for KX1 be SimplicialComplexStr of X st KX1 = (Fnm . m) holds (Fnm . (m + 1)) = ( subdivision (P,KX1)) by Def21;

      defpred R[ Nat] means $1 <= n implies (Fn . $1) = (Fnm . ($1 + k)) & ex SX be SimplicialComplexStr of X st (Fn . $1) = SX;

      

       A7: for m be Nat st R[m] holds R[(m + 1)]

      proof

        let m be Nat such that

         A8: R[m];

        assume

         A9: (m + 1) <= n;

        then

        consider SX be SimplicialComplexStr of X such that

         A10: (Fn . m) = SX by A8, NAT_1: 13;

        ( subdivision (P,SX)) = (Fnm . ((m + k) + 1)) by A6, A8, A9, A10, NAT_1: 13;

        hence thesis by A3, A10;

      end;

      consider Fm be Function such that

       A11: (Fm . 0 ) = KX and

       A12: (Fm . k) = ( subdivision (k,P,KX)) and ( dom Fm) = NAT and

       A13: for m be Nat holds for KX1 be SimplicialComplexStr of X st KX1 = (Fm . m) holds (Fm . (m + 1)) = ( subdivision (P,KX1)) by Def21;

      defpred P[ Nat] means $1 <= k implies (Fm . $1) = (Fnm . $1) & ex SX be SimplicialComplexStr of X st (Fm . $1) = SX;

      

       A14: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat such that

         A15: P[m];

        assume

         A16: (m + 1) <= k;

        then

        consider SX be SimplicialComplexStr of X such that

         A17: (Fm . m) = SX by A15, NAT_1: 13;

        ( subdivision (P,SX)) = (Fnm . (m + 1)) by A6, A15, A16, A17, NAT_1: 13;

        hence thesis by A13, A17;

      end;

      

       A18: P[ 0 qua Nat] by A4, A11;

      for k holds P[k] from NAT_1:sch 2( A18, A14);

      then

       A19: R[ 0 qua Nat] by A1, A12;

      for k holds R[k] from NAT_1:sch 2( A19, A7);

      hence thesis by A2, A5;

    end;

    theorem :: SIMPLEX0:64

    ( [#] ( subdivision (n,P,KX))) = ( [#] KX)

    proof

      defpred P[ Nat] means ( [#] ( subdivision ($1,P,KX))) = ( [#] KX);

      

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

      proof

        let n;

        n in NAT by ORDINAL1:def 12;

        

        then

         A2: ( subdivision ((n + 1),P,KX)) = ( subdivision (1,P,( subdivision (n,P,KX)))) by Th63

        .= ( subdivision (P,( subdivision (n,P,KX)))) by Th62;

        assume ( [#] ( subdivision (n,P,KX))) = ( [#] KX);

        hence thesis by A2, Def20;

      end;

      

       A3: P[ 0 qua Nat] by Th61;

      for n holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: SIMPLEX0:65

    ( subdivision (n,P,SX)) is SubSimplicialComplex of ( subdivision (n,P,KX))

    proof

      defpred P[ Nat] means ( subdivision ($1,P,SX)) is SubSimplicialComplex of ( subdivision ($1,P,KX));

      

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

      proof

        let n;

        assume P[n];

        then

        reconsider Pn = ( subdivision (n,P,SX)) as SubSimplicialComplex of ( subdivision (n,P,KX));

        

         A2: n in NAT by ORDINAL1:def 12;

        

        then

         A3: ( subdivision ((n + 1),P,SX)) = ( subdivision (1,P,Pn)) by Th63

        .= ( subdivision (P,Pn)) by Th62;

        ( subdivision ((n + 1),P,KX)) = ( subdivision (1,P,( subdivision (n,P,KX)))) by A2, Th63

        .= ( subdivision (P,( subdivision (n,P,KX)))) by Th62;

        hence thesis by A3, Th58;

      end;

      ( subdivision ( 0 ,P,SX)) = SX by Th61;

      then

       A4: P[ 0 ] by Th61;

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

      hence thesis;

    end;