:: SIMPLEX0 semantic presentation

begin


notation
let X be set ;
antonym  with_empty_element X for  with_non-empty_elements ;
end;

registration
cluster empty  ->  subset-closed for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is subset-closed
proof
let X be set ; ::_thesis: ( X is empty implies X is subset-closed )
assume  X is empty ; ::_thesis: X is subset-closed
then  for x, y being set st x in X & y c= x holds
y in X ;
hence  X is subset-closed by CLASSES1:def_1; ::_thesis: verum
end;
cluster with_empty_element  ->  non empty for set ;
coherence
 for b1 being set st b1 is with_empty_element holds
not b1 is empty by SETFAM_1:def_8;
cluster non empty subset-closed  ->  with_empty_element for set ;
coherence
 for b1 being set st not b1 is empty & b1 is subset-closed holds
b1 is with_empty_element
proof
let X be set ; ::_thesis: ( not X is empty & X is subset-closed implies X is with_empty_element )
assume A1: ( not X is empty & X is subset-closed ) ; ::_thesis: X is with_empty_element
then consider x being set  such that
A2: x in X by XBOOLE_0:def_1;
 {} c= x by XBOOLE_1:2;
then  {} in X by A1, A2, CLASSES1:def_1;
hence  X is with_empty_element ; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster Sub_of_Fin X ->  finite-membered ;
coherence
 Sub_of_Fin X is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( not x in Sub_of_Fin X or x is finite )
assume  x in Sub_of_Fin X ; ::_thesis: x is finite
hence  x is finite by COHSP_1:def_3; ::_thesis: verum
end;
end;

registration
let X be subset-closed set ;
cluster Sub_of_Fin X ->  subset-closed ;
coherence
 Sub_of_Fin X is subset-closed
proof
let x be set ; :: according to CLASSES1:def_1 ::_thesis: for b1 being set holds
( not x in Sub_of_Fin X or not b1 c= x or b1 in Sub_of_Fin X )
let y be set ; ::_thesis: ( not x in Sub_of_Fin X or not y c= x or y in Sub_of_Fin X )
assume  ( x in Sub_of_Fin X & y c= x ) ; ::_thesis: y in Sub_of_Fin X
hence  y in Sub_of_Fin X by CLASSES1:def_1; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:1
for Y being set holds
( Y is subset-closed iff for X being set st X in Y holds
bool X c= Y )
proof
let Y be set ; ::_thesis: ( Y is subset-closed iff for X being set st X in Y holds
bool X c= Y )
hereby  ::_thesis: ( ( for X being set st X in Y holds
bool X c= Y ) implies Y is subset-closed )
assume A1: Y is subset-closed ; ::_thesis: for X being set st X in Y holds
bool X c= Y
let X be set ; ::_thesis: ( X in Y implies bool X c= Y )
assume A2: X in Y ; ::_thesis: bool X c= Y
thus  bool X c= Y ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool X or x in Y )
assume  x in bool X ; ::_thesis: x in Y
hence  x in Y by A1, A2, CLASSES1:def_1; ::_thesis: verum
end;
end;
assume A3: for X being set st X in Y holds
bool X c= Y ; ::_thesis: Y is subset-closed
let x be set ; :: according to CLASSES1:def_1 ::_thesis: for b1 being set holds
( not x in Y or not b1 c= x or b1 in Y )
let y be set ; ::_thesis: ( not x in Y or not y c= x or y in Y )
assume that
A4: x in Y and
A5: y c= x ; ::_thesis: y in Y
A6: y in bool x by A5;
 bool x c= Y by A3, A4;
hence  y in Y by A6; ::_thesis: verum
end;

registration
let A, B be subset-closed set ;
clusterA \/ B ->  subset-closed ;
coherence
 A \/ B is subset-closed
proof
let x be set ; :: according to CLASSES1:def_1 ::_thesis: for b1 being set holds
( not x in A \/ B or not b1 c= x or b1 in A \/ B )
let y be set ; ::_thesis: ( not x in A \/ B or not y c= x or y in A \/ B )
assume that
A1: x in A \/ B and
A2: y c= x ; ::_thesis: y in A \/ B
 ( 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; ::_thesis: verum
end;
clusterA /\ B ->  subset-closed ;
coherence
 A /\ B is subset-closed
proof
let x be set ; :: according to CLASSES1:def_1 ::_thesis: for b1 being set holds
( not x in A /\ B or not b1 c= x or b1 in A /\ B )
let y be set ; ::_thesis: ( not x in A /\ B or not y c= x or y in A /\ B )
assume that
A3: x in A /\ B and
A4: y c= x ; ::_thesis: y in A /\ B
 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; ::_thesis: verum
end;
end;

Lm1:  for X being set ex F being subset-closed set st
( F = union  {  (bool x) where x is Element of X : x in X  }  & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) )
proof
let X be set ; ::_thesis: ex F being subset-closed set st
( F = union  {  (bool x) where x is Element of X : x in X  }  & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) )
set B =  {  (bool x) where x is Element of X : x in X  }  ;
now__::_thesis:_for_a,_b_being_set_st_a_in_union__{__(bool_x)_where_x_is_Element_of_X_:_x_in_X__}__&_b_c=_a_holds_
b_in_union__{__(bool_x)_where_x_is_Element_of_X_:_x_in_X__}_
let a, b be set ; ::_thesis: ( a in union  {  (bool x) where x is Element of X : x in X  }  & b c= a implies b in union  {  (bool x) where x is Element of X : x in X  }  )
assume that
A1: a in union  {  (bool x) where x is Element of X : x in X  }  and
A2: b c= a ; ::_thesis: b in union  {  (bool x) where x is Element of X : x in X  }
consider y being set  such that
A3: a in y and
A4: y in  {  (bool x) where x is Element of X : x in X  }  by A1, TARSKI:def_4;
consider x being 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  {  (bool x) where x is Element of X : x in X  }  by A4, A5, TARSKI:def_4; ::_thesis: verum
end;
then reconsider U = union  {  (bool x) where x is Element of X : x in X  }  as subset-closed set by CLASSES1:def_1;
take  U ; ::_thesis: ( U = union  {  (bool x) where x is Element of X : x in X  }  & X c= U & ( for Y being set st X c= Y & Y is subset-closed holds
U c= Y ) )
thus  U = union  {  (bool x) where x is Element of X : x in X  }  ; ::_thesis: ( X c= U & ( for Y being set st X c= Y & Y is subset-closed holds
U c= Y ) )
thus  X c= U ::_thesis: for Y being set st X c= Y & Y is subset-closed holds
U c= Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in U )
assume A6: x in X ; ::_thesis: x in U
 ( x c= x & bool x in  {  (bool x) where x is Element of X : x in X  }  ) by A6;
hence  x in U by TARSKI:def_4; ::_thesis: verum
end;
let Y be set ; ::_thesis: ( X c= Y & Y is subset-closed implies U c= Y )
assume A7: ( X c= Y & Y is subset-closed ) ; ::_thesis: U c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U or x in Y )
assume  x in U ; ::_thesis: x in Y
then consider y being set  such that
A8: x in y and
A9: y in  {  (bool x) where x is Element of X : x in X  }  by TARSKI:def_4;
 ex x being Element of X st
( y = bool x & x in X ) by A9;
hence  x in Y by A7, A8, CLASSES1:def_1; ::_thesis: verum
end;

definition
let X be set ;
func subset-closed_closure_of X ->  subset-closed set  means :Def1: :: SIMPLEX0:def 1
( X c= it & ( for Y being set st X c= Y & Y is subset-closed holds
it c= Y ) );
existence
 ex b1 being subset-closed set st
( X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds
b1 c= Y ) )
proof
 ex F being subset-closed set st
( F = union  {  (bool x) where x is Element of X : x in X  }  & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) ) by Lm1;
hence  ex b1 being subset-closed set st
( X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds
b1 c= Y ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being subset-closed set st X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds
b1 c= Y ) & X c= b2 & ( for Y being set st X c= Y & Y is subset-closed holds
b2 c= Y ) holds
b1 = b2
proof
let F1, F2 be subset-closed set ; ::_thesis: ( X c= F1 & ( for Y being set st X c= Y & Y is subset-closed holds
F1 c= Y ) & X c= F2 & ( for Y being set st X c= Y & Y is subset-closed holds
F2 c= Y ) implies F1 = F2 )
assume  ( X c= F1 & ( for Y being set st X c= Y & Y is subset-closed holds
F1 c= Y ) & X c= F2 & ( for Y being set st X c= Y & Y is subset-closed holds
F2 c= Y ) ) ; ::_thesis: F1 = F2
then  ( F1 c= F2 & F2 c= F1 ) ;
hence  F1 = F2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def_1_:_
 for X being set
for b2 being subset-closed set holds
( b2 = subset-closed_closure_of X iff ( X c= b2 & ( for Y being set st X c= Y & Y is subset-closed holds
b2 c= Y ) ) );

theorem Th2: :: SIMPLEX0:2
for x, X being set holds
( x in subset-closed_closure_of X iff ex y being set st
( x c= y & y in X ) )
proof
let x, X be set ; ::_thesis: ( x in subset-closed_closure_of X iff ex y being set st
( x c= y & y in X ) )
set B =  {  (bool x1) where x1 is Element of X : x1 in X  }  ;
consider F being subset-closed set  such that
A1: F = union  {  (bool x1) where x1 is Element of X : x1 in X  }  and
A2: ( X c= F & ( for Y being set 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  ::_thesis: ( ex y being set st
( x c= y & y in X ) implies x in subset-closed_closure_of X )
assume  x in subset-closed_closure_of X ; ::_thesis: ex y being set st
( x c= y & y in X )
then consider y being set  such that
A4: x in y and
A5: y in  {  (bool x1) where x1 is Element of X : x1 in X  }  by A1, A3, TARSKI:def_4;
consider x1 being Element of X such that
A6: ( bool x1 = y & x1 in X ) by A5;
reconsider y = x1 as set ;
take y = y; ::_thesis: ( x c= y & y in X )
thus  ( x c= y & y in X ) by A4, A6; ::_thesis: verum
end;
given y being set  such that A7: x c= y and
A8: y in X ; ::_thesis: x in subset-closed_closure_of X
 bool y in  {  (bool x1) where x1 is Element of X : x1 in X  }  by A8;
hence  x in subset-closed_closure_of X by A1, A3, A7, TARSKI:def_4; ::_thesis: verum
end;

definition
let X be set ;
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
 subset-closed_closure_of F is subset-closed Subset-Family of X
proof
set FIC = subset-closed_closure_of F;
 subset-closed_closure_of F c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in subset-closed_closure_of F or x in bool X )
assume  x in subset-closed_closure_of F ; ::_thesis: x in bool X
then  ex y being set st
( x c= y & y in F ) by Th2;
then  x c= X by XBOOLE_1:1;
hence  x in bool X ; ::_thesis: verum
end;
hence  subset-closed_closure_of F is subset-closed Subset-Family of X ; ::_thesis: verum
end;
end;

registration
cluster subset-closed_closure_of {} ->  empty subset-closed ;
coherence
 subset-closed_closure_of {} is empty
proof
assume  not subset-closed_closure_of {} is empty ; ::_thesis: contradiction
then consider x being set  such that
A1: x in subset-closed_closure_of {} by XBOOLE_0:def_1;
 ex y being set st
( x c= y & y in {} ) by A1, Th2;
hence  contradiction ; ::_thesis: verum
end;
let X be non empty set ;
cluster subset-closed_closure_of X ->  non empty subset-closed ;
coherence
 not subset-closed_closure_of X is empty
proof
 ex x being set st x in X by XBOOLE_0:def_1;
hence  not subset-closed_closure_of X is empty by Th2; ::_thesis: verum
end;
end;

registration
let X be with_non-empty_element set ;
cluster subset-closed_closure_of X ->  with_non-empty_element subset-closed ;
coherence
 not subset-closed_closure_of X is empty-membered
proof
consider b being 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  not subset-closed_closure_of X is empty-membered by SETFAM_1:def_10; ::_thesis: verum
end;
end;

registration
let X be finite-membered set ;
cluster subset-closed_closure_of X ->  finite-membered subset-closed ;
coherence
 subset-closed_closure_of X is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( not x in subset-closed_closure_of X or x is finite )
assume  x in subset-closed_closure_of X ; ::_thesis: x is finite
then consider y being set  such that
A1: x c= y and
A2: y in X by Th2;
 y is finite by A2;
hence  x is finite by A1; ::_thesis: verum
end;
end;

theorem Th3: :: SIMPLEX0:3
for X, Y being set st X c= Y & Y is subset-closed holds
subset-closed_closure_of X c= Y
proof
let X, Y be set ; ::_thesis: ( X c= Y & Y is subset-closed implies subset-closed_closure_of X c= Y )
assume A1: ( X c= Y & Y is subset-closed ) ; ::_thesis: subset-closed_closure_of X c= Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in subset-closed_closure_of X or x in Y )
assume  x in subset-closed_closure_of X ; ::_thesis: x in Y
then  ex y being set st
( x c= y & y in X ) by Th2;
hence  x in Y by A1, CLASSES1:def_1; ::_thesis: verum
end;

theorem Th4: :: SIMPLEX0:4
for X being set holds subset-closed_closure_of {X} = bool X
proof
let X be set ; ::_thesis: subset-closed_closure_of {X} = bool X
set f = subset-closed_closure_of {X};
A1: X in {X} by TARSKI:def_1;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: bool X c= subset-closed_closure_of {X}
let x be set ; ::_thesis: ( x in subset-closed_closure_of {X} implies x in bool X )
assume  x in subset-closed_closure_of {X} ; ::_thesis: x in bool X
then consider y being set  such that
A2: x c= y and
A3: y in {X} by Th2;
 y = X by A3, TARSKI:def_1;
hence  x in bool X by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool X or x in subset-closed_closure_of {X} )
assume  x in bool X ; ::_thesis: x in subset-closed_closure_of {X}
hence  x in subset-closed_closure_of {X} by A1, Th2; ::_thesis: verum
end;

theorem :: SIMPLEX0:5
for X, Y being set holds subset-closed_closure_of (X \/ Y) = (subset-closed_closure_of X) \/ (subset-closed_closure_of Y)
proof
let X, Y be set ; ::_thesis: subset-closed_closure_of (X \/ Y) = (subset-closed_closure_of X) \/ (subset-closed_closure_of Y)
set fxy = subset-closed_closure_of (X \/ Y);
set fx = subset-closed_closure_of X;
set fy = subset-closed_closure_of Y;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) c= subset-closed_closure_of (X \/ Y)
let x be set ; ::_thesis: ( x in subset-closed_closure_of (X \/ Y) implies x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) )
assume  x in subset-closed_closure_of (X \/ Y) ; ::_thesis: x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y)
then consider y being set  such that
A1: x 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 subset-closed_closure_of X or x in subset-closed_closure_of Y ) by A1, Th2;
hence  x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) or x in subset-closed_closure_of (X \/ Y) )
assume A3: x in (subset-closed_closure_of X) \/ (subset-closed_closure_of Y) ; ::_thesis: x in subset-closed_closure_of (X \/ Y)
percases ( x in subset-closed_closure_of X or x in subset-closed_closure_of Y ) by A3, XBOOLE_0:def_3;
suppose x in subset-closed_closure_of X ; ::_thesis: x in subset-closed_closure_of (X \/ Y)
then consider y being set  such that
A4: x c= y and
A5: y in X by Th2;
 y in X \/ Y by A5, XBOOLE_0:def_3;
hence  x in subset-closed_closure_of (X \/ Y) by A4, Th2; ::_thesis: verum
end;
suppose x in subset-closed_closure_of Y ; ::_thesis: x in subset-closed_closure_of (X \/ Y)
then consider y being set  such that
A6: x c= y and
A7: y in Y by Th2;
 y in X \/ Y by A7, XBOOLE_0:def_3;
hence  x in subset-closed_closure_of (X \/ Y) by A6, Th2; ::_thesis: verum
end;
end;
end;

theorem Th6: :: SIMPLEX0:6
for X, Y being set holds
( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y )
proof
let X, Y be set ; ::_thesis: ( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y )
set fx = subset-closed_closure_of X;
set fy = subset-closed_closure_of Y;
hereby  ::_thesis: ( subset-closed_closure_of X c= subset-closed_closure_of Y implies X is_finer_than Y )
assume A1: X is_finer_than Y ; ::_thesis: subset-closed_closure_of X c= subset-closed_closure_of Y
thus  subset-closed_closure_of X c= subset-closed_closure_of Y ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in subset-closed_closure_of X or x in subset-closed_closure_of Y )
assume  x in subset-closed_closure_of X ; ::_thesis: x in subset-closed_closure_of Y
then consider y being set  such that
A2: x c= y and
A3: y in X by Th2;
consider c being set  such that
A4: c in Y and
A5: y c= c by A1, A3, SETFAM_1:def_2;
 x c= c by A2, A5, XBOOLE_1:1;
hence  x in subset-closed_closure_of Y by A4, Th2; ::_thesis: verum
end;
end;
assume A6: subset-closed_closure_of X c= subset-closed_closure_of Y ; ::_thesis: X is_finer_than Y
let x be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not x in X or ex b1 being set st
( b1 in Y & x c= b1 ) )
assume  x in X ; ::_thesis: ex b1 being set st
( b1 in Y & x c= b1 )
then  x in subset-closed_closure_of X by Th2;
then  ex y being set st
( x c= y & y in Y ) by A6, Th2;
hence  ex b1 being set st
( b1 in Y & x c= b1 ) ; ::_thesis: verum
end;

theorem Th7: :: SIMPLEX0:7
for X being set st X is subset-closed holds
subset-closed_closure_of X = X
proof
let X be set ; ::_thesis: ( X is subset-closed implies subset-closed_closure_of X = X )
set f = subset-closed_closure_of X;
assume A1: X is subset-closed ; ::_thesis: subset-closed_closure_of X = X
thus  subset-closed_closure_of X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= subset-closed_closure_of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in subset-closed_closure_of X or x in X )
assume  x in subset-closed_closure_of X ; ::_thesis: x in X
then  ex y being set st
( x c= y & y in X ) by Th2;
hence  x in X by A1, CLASSES1:def_1; ::_thesis: verum
end;
thus  X c= subset-closed_closure_of X by Def1; ::_thesis: verum
end;

theorem :: SIMPLEX0:8
for X being set st subset-closed_closure_of X c= X holds
X is subset-closed
proof
let X be set ; ::_thesis: ( subset-closed_closure_of X c= X implies X is subset-closed )
set f = subset-closed_closure_of X;
assume A1: subset-closed_closure_of X c= X ; ::_thesis: X is subset-closed
let x be set ; :: according to CLASSES1:def_1 ::_thesis: for b1 being set holds
( not x in X or not b1 c= x or b1 in X )
let y be set ; ::_thesis: ( not x in X or not y c= x or y in X )
assume  ( x in X & y c= x ) ; ::_thesis: y in X
then  y in subset-closed_closure_of X by Th2;
hence  y in X by A1; ::_thesis: verum
end;

definition
let Y, X, n be set ;
func the_subsets_with_limited_card (n,X,Y) ->  Subset-Family of Y means :Def2: :: SIMPLEX0:def 2
 for A being Subset of Y holds
( A in it iff ( A in X & card A c= card n ) );
existence
 ex b1 being Subset-Family of Y st
for A being Subset of Y holds
( A in b1 iff ( A in X & card A c= card n ) )
proof
set SS =  {  A where A is Subset of Y : ( A in X & card A c= card n )  }  ;
  {  A where A is Subset of Y : ( A in X & card A c= card n )  }  c= bool Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of Y : ( A in X & card A c= card n )  }  or x in bool Y )
assume  x in  {  A where A is Subset of Y : ( A in X & card A c= card n )  }  ; ::_thesis: x in bool Y
then  ex A being Subset of Y st
( x = A & A in X & card A c= card n ) ;
hence  x in bool Y ; ::_thesis: verum
end;
then reconsider SS =  {  A where A is Subset of Y : ( A in X & card A c= card n )  }  as Subset-Family of Y ;
take  SS ; ::_thesis: for A being Subset of Y holds
( A in SS iff ( A in X & card A c= card n ) )
let A be Subset of Y; ::_thesis: ( A in SS iff ( A in X & card A c= card n ) )
hereby  ::_thesis: ( A in X & card A c= card n implies A in SS )
assume  A in SS ; ::_thesis: ( A in X & card A c= card n )
then  ex B being Subset of Y st
( B = A & B in X & card B c= card n ) ;
hence  ( A in X & card A c= card n ) ; ::_thesis: verum
end;
assume  ( A in X & card A c= card n ) ; ::_thesis: A in SS
hence  A in SS ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of Y st ( for A being Subset of Y holds
( A in b1 iff ( A in X & card A c= card n ) ) ) & ( for A being Subset of Y holds
( A in b2 iff ( A in X & card A c= card n ) ) ) holds
b1 = b2
proof
let S1, S2 be Subset-Family of Y; ::_thesis: ( ( for A being Subset of Y holds
( A in S1 iff ( A in X & card A c= card n ) ) ) & ( for A being Subset of Y holds
( A in S2 iff ( A in X & card A c= card n ) ) ) implies S1 = S2 )
assume that
A1: for A being Subset of Y holds
( A in S1 iff ( A in X & card A c= card n ) ) and
A2: for A being Subset of Y holds
( A in S2 iff ( A in X & card A c= card n ) ) ; ::_thesis: S1 = S2
thus  S1 c= S2 :: according to XBOOLE_0:def_10 ::_thesis: S2 c= S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S1 or x in S2 )
assume A3: x in S1 ; ::_thesis: x in S2
then  ( x in X & card x c= card n ) by A1;
hence  x in S2 by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S2 or x in S1 )
assume A4: x in S2 ; ::_thesis: x in S1
then  ( x in X & card x c= card n ) by A2;
hence  x in S1 by A1, A4; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines the_subsets_with_limited_card SIMPLEX0:def_2_:_
 for Y, X, n being set
for b4 being Subset-Family of Y holds
( b4 = the_subsets_with_limited_card (n,X,Y) iff for A being Subset of Y holds
( A in b4 iff ( A in X & card A c= card n ) ) );

registration
let D be non empty set ;
cluster with_non-empty_element finite finite-membered subset-closed for Element of bool (bool D);
existence
 ex b1 being Subset-Family of D st
( b1 is finite & b1 is with_non-empty_element & b1 is subset-closed & b1 is finite-membered )
proof
consider x being set  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 ; ::_thesis: ( XX is finite & XX is with_non-empty_element & XX is subset-closed & XX is finite-membered )
 {x} in bool {x} by ZFMISC_1:def_1;
hence  ( XX is finite & XX is with_non-empty_element & XX is subset-closed & XX is finite-membered ) by SETFAM_1:def_10; ::_thesis: verum
end;
end;

registration
let Y, X be set ;
let n be finite set ;
cluster the_subsets_with_limited_card (n,X,Y) ->  finite-membered ;
coherence
 the_subsets_with_limited_card (n,X,Y) is finite-membered
proof
let A be set ; :: according to FINSET_1:def_6 ::_thesis: ( not A in the_subsets_with_limited_card (n,X,Y) or A is finite )
assume  A in the_subsets_with_limited_card (n,X,Y) ; ::_thesis: A is finite
then  card A c= card n by Def2;
hence  A is finite ; ::_thesis: verum
end;
end;

registration
let Y be set ;
let X be subset-closed set ;
let n be set ;
cluster the_subsets_with_limited_card (n,X,Y) ->  subset-closed ;
coherence
 the_subsets_with_limited_card (n,X,Y) is subset-closed
proof
let x be set ; :: according to CLASSES1:def_1 ::_thesis: for b1 being set holds
( not x in the_subsets_with_limited_card (n,X,Y) or not b1 c= x or b1 in the_subsets_with_limited_card (n,X,Y) )
let y be set ; ::_thesis: ( not x in the_subsets_with_limited_card (n,X,Y) or not y c= x or y in the_subsets_with_limited_card (n,X,Y) )
assume that
A1: x in the_subsets_with_limited_card (n,X,Y) and
A2: y c= x ; ::_thesis: y in the_subsets_with_limited_card (n,X,Y)
 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 by XBOOLE_1:1;
 y c= Y by A1, A2, XBOOLE_1:1;
hence  y in the_subsets_with_limited_card (n,X,Y) by A3, A4, Def2; ::_thesis: verum
end;
end;

registration
let Y be set ;
let X be with_empty_element set ;
let n be set ;
cluster the_subsets_with_limited_card (n,X,Y) ->  with_empty_element ;
coherence
 the_subsets_with_limited_card (n,X,Y) is with_empty_element
proof
A1: {} c= Y by XBOOLE_1:2;
 ( 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  the_subsets_with_limited_card (n,X,Y) is with_empty_element ; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
let X be with_non-empty_element subset-closed Subset-Family of D;
let n be non empty set ;
cluster the_subsets_with_limited_card (n,X,D) ->  with_non-empty_element ;
coherence
 not the_subsets_with_limited_card (n,X,D) is empty-membered
proof
consider x being non empty set  such that
A1: x in X by SETFAM_1:def_10;
consider y being set  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  not the_subsets_with_limited_card (n,X,D) is empty-membered by SETFAM_1:def_10; ::_thesis: verum
end;
end;

notation
let X be set ;
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 Th9: :: SIMPLEX0:9
for X being set st not X is empty & X is finite & X is c=-linear holds
union X in X
proof
let X be set ; ::_thesis: ( not X is empty & X is finite & X is c=-linear implies union X in X )
assume  ( not X is empty & X is finite & X is c=-linear ) ; ::_thesis: union X in X
then consider U being set  such that
A1: U in X and
A2: for x being set st x in X holds
x c= U by FINSET_1:12;
A3: union X c= U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union X or x in U )
assume  x in union X ; ::_thesis: x in U
then consider y being set  such that
A4: x in y and
A5: y in X by TARSKI:def_4;
 y c= U by A2, A5;
hence  x in U by A4; ::_thesis: verum
end;
 U c= union X by A1, ZFMISC_1:74;
hence  union X in X by A1, A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th10: :: SIMPLEX0:10
for X being c=-linear finite set st X is with_non-empty_elements holds
card X c= card (union X)
proof
let X be c=-linear finite set ; ::_thesis: ( X is with_non-empty_elements implies card X c= card (union X) )
defpred S1[ Nat] means  for X being c=-linear finite set st X is with_non-empty_elements & card (union X) = $1 holds
card X c= card (union X);
defpred S2[ Nat] means  for n being Nat st n <= $1 holds
S1[n];
assume A1: X is with_non-empty_elements ; ::_thesis: card X c= card (union X)
A2: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A3: S2[m] ; ::_thesis: S2[m + 1]
let n be Nat; ::_thesis: ( n <= m + 1 implies S1[n] )
assume A4: n <= m + 1 ; ::_thesis: S1[n]
let X be c=-linear finite set ; ::_thesis: ( X is with_non-empty_elements & card (union X) = n implies card X c= card (union X) )
assume that
A5: X is with_non-empty_elements and
A6: card (union X) = n ; ::_thesis: card X c= card (union X)
reconsider u = union X as finite set by A6;
reconsider Xu = X \ {u} as c=-linear finite set ;
percases ( n <= m or n = m + 1 ) by A4, NAT_1:8;
suppose n <= m ; ::_thesis: card X c= card (union X)
hence  card X c= card (union X) by A3, A5, A6; ::_thesis: verum
end;
supposeA7: n = m + 1 ; ::_thesis: card X c= card (union X)
then  not X is 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 ; ::_thesis: contradiction
then  not Xu is empty by A6, A7, ZFMISC_1:2;
then  u in Xu by A10, Th9;
hence  contradiction by ZFMISC_1:56; ::_thesis: verum
end;
then A11: uXu c< u by A9, XBOOLE_0:def_8;
then  card uXu < m + 1 by A6, A7, CARD_2:48;
then  card uXu <= m by NAT_1:13;
then  card Xu c= 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  1 + (card Xu) = card X by A8, CARD_2:41;
hence  card X c= card (union X) by A12, NAT_1:39; ::_thesis: verum
end;
end;
end;
A13: S2[ 0 ]
proof
let n be Nat; ::_thesis: ( n <= 0 implies S1[n] )
assume A14: n <= 0 ; ::_thesis: S1[n]
let X be c=-linear finite set ; ::_thesis: ( X is with_non-empty_elements & card (union X) = n implies card X c= card (union X) )
assume A15: ( X is with_non-empty_elements & card (union X) = n ) ; ::_thesis: card X c= card (union X)
 X is empty by A14, A15;
hence  card X c= card (union X) ; ::_thesis: verum
end;
 for n being Nat holds S2[n] from NAT_1:sch_2(A13, A2);
hence  card X c= card (union X) by A1; ::_thesis: verum
end;

theorem :: SIMPLEX0:11
for X, x being set st X is c=-linear holds
X \/ {((union X) \/ x)} is c=-linear
proof
let X, x be set ; ::_thesis: ( X is c=-linear implies X \/ {((union X) \/ x)} is c=-linear )
assume A1: X is c=-linear ; ::_thesis: X \/ {((union X) \/ x)} is c=-linear
set U = union X;
set Ux = (union X) \/ x;
A2: union X c= (union X) \/ x by XBOOLE_1:7;
let x1, x2 be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not x1 in X \/ {((union X) \/ x)} or not x2 in X \/ {((union X) \/ x)} or x1,x2 are_c=-comparable )
assume A3: ( x1 in X \/ {((union X) \/ x)} & x2 in X \/ {((union X) \/ x)} ) ; ::_thesis: x1,x2 are_c=-comparable
percases ( ( x1 in X & x2 in X ) or ( x1 in {((union X) \/ x)} & x2 in {((union X) \/ x)} ) or ( x1 in X & x2 in {((union X) \/ x)} ) or ( x2 in X & x1 in {((union X) \/ x)} ) ) by A3, XBOOLE_0:def_3;
suppose ( x1 in X & x2 in X ) ; ::_thesis: x1,x2 are_c=-comparable
hence  x1,x2 are_c=-comparable by A1, ORDINAL1:def_8; ::_thesis: verum
end;
supposeA4: ( x1 in {((union X) \/ x)} & x2 in {((union X) \/ x)} ) ; ::_thesis: x1,x2 are_c=-comparable
then  x1 = (union X) \/ x by TARSKI:def_1;
hence  x1,x2 are_c=-comparable by A4, TARSKI:def_1; ::_thesis: verum
end;
suppose ( x1 in X & x2 in {((union X) \/ x)} ) ; ::_thesis: x1,x2 are_c=-comparable
then  ( x1 c= union X & x2 = (union X) \/ x ) by TARSKI:def_1, ZFMISC_1:74;
then  x1 c= x2 by A2, XBOOLE_1:1;
hence  x1,x2 are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
suppose ( x2 in X & x1 in {((union X) \/ x)} ) ; ::_thesis: x1,x2 are_c=-comparable
then  ( x2 c= union X & x1 = (union X) \/ x ) by TARSKI:def_1, ZFMISC_1:74;
then  x2 c= x1 by A2, XBOOLE_1:1;
hence  x1,x2 are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
end;
end;

theorem Th12: :: SIMPLEX0:12
for X being non empty set ex Y being Subset-Family of X st
( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
proof
let X be non empty set ; ::_thesis: ex Y being Subset-Family of X st
( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
consider R being Relation such that
A1: R well_orders X by WELLORD2:17;
set RX = R |_2 X;
deffunc H1( set ) ->  Element of bool X = X \ ((R |_2 X) -Seg $1);
A2: for x being set st x in X holds
H1(x) in bool X ;
consider f being Function of X,(bool X) such that
A3: for x being set st x in X holds
f . x = H1(x) from FUNCT_2:sch_2(A2);
take Y = rng f; ::_thesis: ( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
A4: dom f = X by FUNCT_2:def_1;
thus  Y is with_non-empty_elements ::_thesis: ( Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
proof
assume  Y is with_empty_element ; ::_thesis: contradiction
then  {} in Y by SETFAM_1:def_8;
then consider x being set  such that
A5: x in dom f and
A6: f . x = {} by FUNCT_1:def_3;
 {} = H1(x) by A3, A5, A6;
then  X c= (R |_2 X) -Seg x by XBOOLE_1:37;
hence  contradiction by A4, A5, WELLORD1:1; ::_thesis: verum
end;
thus  Y is c=-linear ::_thesis: ( X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
proof
let x be set ; :: according to ORDINAL1:def_8 ::_thesis: for b1 being set holds
( not x in Y or not b1 in Y or x,b1 are_c=-comparable )
let y be set ; ::_thesis: ( not x in Y or not y in Y or x,y are_c=-comparable )
assume that
A7: x in Y and
A8: y in Y ; ::_thesis: x,y are_c=-comparable
consider a being set  such that
A9: ( a in dom f & f . a = x ) by A7, FUNCT_1:def_3;
consider b being set  such that
A10: ( b in dom f & f . b = y ) by A8, FUNCT_1:def_3;
 (R |_2 X) -Seg a,(R |_2 X) -Seg b are_c=-comparable by A1, WELLORD1:26, WELLORD2:16;
then  ( (R |_2 X) -Seg a c= (R |_2 X) -Seg b or (R |_2 X) -Seg b c= (R |_2 X) -Seg a ) by XBOOLE_0:def_9;
then  ( H1(b) c= H1(a) or H1(a) c= H1(b) ) by XBOOLE_1:34;
then A11: H1(a),H1(b) are_c=-comparable by XBOOLE_0:def_9;
 x = H1(a) by A3, A9;
hence  x,y are_c=-comparable by A3, A10, A11; ::_thesis: verum
end;
A12: field (R |_2 X) = X by A1, WELLORD2:16;
then consider x being set  such that
A13: x in X and
A14: for y being set st y in X holds
[x,y] in R |_2 X by A1, WELLORD1:7, WELLORD2:16;
A15: R |_2 X is well-ordering by A1, WELLORD2:16;
then A16: R |_2 X is well_founded by WELLORD1:def_4;
 R |_2 X is antisymmetric by A15, WELLORD1:def_4;
then A17: R |_2 X is_antisymmetric_in X by A12, RELAT_2:def_12;
A18: (R |_2 X) -Seg x = {}
proof
assume  (R |_2 X) -Seg x <> {} ; ::_thesis: contradiction
then consider y being set  such that
A19: y in (R |_2 X) -Seg x by XBOOLE_0:def_1;
A20: y <> x by A19, WELLORD1:1;
A21: [y,x] in R |_2 X 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 R |_2 X by A14;
hence  contradiction by A17, A20, A21, A22, A23, RELAT_2:def_4; ::_thesis: verum
end;
 f . x = H1(x) by A3, A13;
hence  X in Y by A4, A13, A18, FUNCT_1:def_3; ::_thesis: ( card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_X_&_x2_in_X_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in X & x2 in X & f . x1 = f . x2 implies x1 = x2 )
reconsider R1 = (R |_2 X) -Seg x1, R2 = (R |_2 X) -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 ; ::_thesis: x1 = x2
 ( R1 ` = f . x1 & f . x2 = R2 ` ) by A3, A24;
then  R1 = R2 by A25, SUBSET_1:42;
then  ( [x1,x2] in R |_2 X & [x2,x1] in R |_2 X ) by A12, A15, A24, WELLORD1:29;
hence  x1 = x2 by A17, A24, RELAT_2:def_4; ::_thesis: verum
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; ::_thesis: for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y )
let Z be set ; ::_thesis: ( Z in Y & card Z <> 1 implies ex x being set st
( x in Z & Z \ {x} in Y ) )
assume that
A26: Z in Y and
A27: card Z <> 1 ; ::_thesis: ex x being set st
( x in Z & Z \ {x} in Y )
consider x being set  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;
take  x ; ::_thesis: ( x in Z & Z \ {x} in Y )
A31: not x in (R |_2 X) -Seg x by WELLORD1:1;
A32: Z = X \ ((R |_2 X) -Seg x) by A3, A28, A29;
hence  x in Z by A28, A31, XBOOLE_0:def_5; ::_thesis: Z \ {x} in Y
 (R |_2 X) -Seg x c= X by A12, WELLORD1:9;
then reconsider Rxx = ((R |_2 X) -Seg x) \/ {x} as Subset of X by A30, XBOOLE_1:8;
 X \ Rxx <> {}
proof
assume  X \ Rxx = {} ; ::_thesis: contradiction
then  X c= Rxx by XBOOLE_1:37;
then Z = Rxx \ ((R |_2 X) -Seg x) by A32, XBOOLE_0:def_10
.= {x} \ ((R |_2 X) -Seg x) by XBOOLE_1:40
.= {x} by A31, ZFMISC_1:59 ;
hence  contradiction by A27, CARD_1:30; ::_thesis: verum
end;
then consider a being set  such that
A33: a in Rxx ` and
A34: (R |_2 X) -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;
 R |_2 X is connected by A15, WELLORD1:def_4;
then  R |_2 X is_connected_in X by A12, RELAT_2:def_14;
then A37: ( [x,a] in R |_2 X or [a,x] in R |_2 X ) by A28, A33, A36, RELAT_2:def_6;
A38: not a in (R |_2 X) -Seg x by A35, XBOOLE_0:def_3;
then  x in (R |_2 X) -Seg a by A36, A37, WELLORD1:1;
then A39: {x} c= (R |_2 X) -Seg a by ZFMISC_1:31;
 (R |_2 X) -Seg a c= X by A12, WELLORD1:9;
then A40: (R |_2 X) -Seg a c= Rxx by A34, SUBSET_1:24;
 (R |_2 X) -Seg x c= (R |_2 X) -Seg a by A12, A15, A28, A33, A37, A38, WELLORD1:1, WELLORD1:29;
then  Rxx c= (R |_2 X) -Seg a by A39, XBOOLE_1:8;
then  Rxx = (R |_2 X) -Seg a by A40, XBOOLE_0:def_10;
then f . a = X \ Rxx by A3, A33
.= (X \ ((R |_2 X) -Seg x)) \ {x} by XBOOLE_1:41
.= Z \ {x} by A3, A28, A29 ;
hence  Z \ {x} in Y by A4, A33, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: SIMPLEX0:13
for X being set
for Y being Subset-Family of X st Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y holds
ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )
proof
let X be set ; ::_thesis: for Y being Subset-Family of X st Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y holds
ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )
let Y be Subset-Family of X; ::_thesis: ( Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y implies ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) ) )
assume that
A1: ( Y is finite & Y is with_non-empty_elements & Y is c=-linear ) and
A2: X in Y ; ::_thesis: ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )
defpred S1[ set , set ] means ( $1 in $2 & $2 in Y & ( for y being set st y in Y & $1 in y holds
$2 c= y ) );
A3: for x being set st x in X holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st S1[x,y] )
set U =  {  A where A is Subset of X : ( x in A & A in Y )  }  ;
A4:  {  A where A is Subset of X : ( x in A & A in Y )  }  c= Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  A where A is Subset of X : ( x in A & A in Y )  }  or y in Y )
assume  y in  {  A where A is Subset of X : ( x in A & A in Y )  }  ; ::_thesis: y in Y
then  ex A being Subset of X st
( y = A & x in A & A in Y ) ;
hence  y in Y ; ::_thesis: verum
end;
then reconsider U =  {  A where A is Subset of X : ( x in A & A in Y )  }  as Subset-Family of X by XBOOLE_1:1;
assume  x in X ; ::_thesis: ex y being set st S1[x,y]
then  X in U by A2;
then consider m being set  such that
A5: m in U and
A6: for y being set st y in U holds
m c= y by A1, A4, FINSET_1:11;
take  m ; ::_thesis: S1[x,m]
 ex A being Subset of X st
( m = A & x in A & A in Y ) by A5;
hence  ( x in m & m in Y ) ; ::_thesis: for y being set st y in Y & x in y holds
m c= y
let y be set ; ::_thesis: ( y in Y & x in y implies m c= y )
assume  ( y in Y & x in y ) ; ::_thesis: m c= y
then  y in U ;
hence  m c= y by A6; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = X & ( for x being set st x in X holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A3);
defpred S2[ set , set ] means ( ( $2 in Y or $2 is empty ) & $2 c< $1 & ( for x being set st x in Y & x c< $1 holds
x c= $2 ) & ( for x being set st x in Y & $2 c= x & x c= $1 & not x = $1 holds
x = $2 ) );
A8: for x being set st x in Y holds
ex y being set st
( y in bool X & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in Y implies ex y being set st
( y in bool X & S2[x,y] ) )
assume A9: x in Y ; ::_thesis: ex y being set st
( y in bool X & S2[x,y] )
set U =  {  A where A is Subset of X : ( A c< x & A in Y )  }  ;
A10:  {  A where A is Subset of X : ( A c< x & A in Y )  }  c= Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  A where A is Subset of X : ( A c< x & A in Y )  }  or y in Y )
assume  y in  {  A where A is Subset of X : ( A c< x & A in Y )  }  ; ::_thesis: y in Y
then  ex A being Subset of X st
( y = A & A c< x & A in Y ) ;
hence  y in Y ; ::_thesis: verum
end;
then reconsider U =  {  A where A is Subset of X : ( A c< x & A in Y )  }  as Subset-Family of X by XBOOLE_1:1;
take u = union U; ::_thesis: ( u in bool X & S2[x,u] )
thus  u in bool X ; ::_thesis: S2[x,u]
A11: for y being set st y in Y & y c< x holds
y c= u
proof
let y be set ; ::_thesis: ( y in Y & y c< x implies y c= u )
assume that
A12: y in Y and
A13: y c< x ; ::_thesis: y c= u
 y in U by A12, A13;
hence  y c= u by ZFMISC_1:74; ::_thesis: verum
end;
percases ( U is empty or not U is empty ) ;
suppose U is empty ; ::_thesis: S2[x,u]
hence  ( ( u in Y or u is empty ) & u c< x & ( for y being set st y in Y & y c< x holds
y c= u ) ) by A1, A9, A11, XBOOLE_1:61, ZFMISC_1:2; ::_thesis: for x being set st x in Y & u c= x & x c= x & not x = x holds
x = u
let y be set ; ::_thesis: ( y in Y & u c= y & y c= x & not y = x implies y = u )
assume that
A14: y in Y and
A15: u c= y and
A16: y c= x ; ::_thesis: ( y = x or y = u )
assume  y <> x ; ::_thesis: y = u
then  y c< x by A16, XBOOLE_0:def_8;
then  y c= u by A11, A14;
hence  y = u by A15, XBOOLE_0:def_10; ::_thesis: verum
end;
suppose not U is empty ; ::_thesis: S2[x,u]
then  u in U by A1, A10, Th9;
then  ex A being Subset of X st
( A = u & A c< x & A in Y ) ;
hence  ( ( u in Y or u is empty ) & u c< x & ( for y being set st y in Y & y c< x holds
y c= u ) ) by A11; ::_thesis: for x being set st x in Y & u c= x & x c= x & not x = x holds
x = u
let y be set ; ::_thesis: ( y in Y & u c= y & y c= x & not y = x implies y = u )
assume that
A17: y in Y and
A18: u c= y and
A19: y c= x ; ::_thesis: ( y = x or y = u )
assume  y <> x ; ::_thesis: y = u
then  y c< x by A19, XBOOLE_0:def_8;
then  y c= u by A11, A17;
hence  y = u by A18, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
consider g being Function of Y,(bool X) such that
A20: for x being set st x in Y holds
S2[x,g . x] from FUNCT_2:sch_1(A8);
defpred S3[ set , set ] means  ex h being Function of ($1 \ (g . $1)),(bool ($1 \ (g . $1))) st
( $2 = h & h is one-to-one & rng h is with_non-empty_elements & rng h is c=-linear & dom h in rng h & ( for Z being set st Z in rng h & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng h ) ) );
A21: for x being set st x in Y holds
ex y being set st S3[x,y]
proof
let y be set ; ::_thesis: ( y in Y implies ex y being set st S3[y,y] )
assume  y in Y ; ::_thesis: ex y being set st S3[y,y]
then  g . y c< y by A20;
then  y \ (g . y) <> {} by XBOOLE_1:105;
then consider Z being Subset-Family of (y \ (g . y)) such that
A22: ( Z is with_non-empty_elements & Z is c=-linear & y \ (g . y) in Z ) and
A23: card (y \ (g . y)) = card Z and
A24: for z being set st z in Z & card z <> 1 holds
ex x being set st
( x in z & z \ {x} in Z ) by Th12;
 y \ (g . y),Z are_equipotent by A23, CARD_1:5;
then consider h being Function such that
A25: h is one-to-one and
A26: ( dom h = y \ (g . y) & rng h = Z ) by WELLORD2:def_4;
reconsider h = h as Function of (y \ (g . y)),(bool (y \ (g . y))) by A26, FUNCT_2:2;
take  h ; ::_thesis: S3[y,h]
thus  S3[y,h] by A22, A24, A25, A26; ::_thesis: verum
end;
consider h being Function such that
A27: ( dom h = Y & ( for x being set st x in Y holds
S3[x,h . x] ) ) from CLASSES1:sch_1(A21);
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_is_Function
let x be set ; ::_thesis: ( x in dom h implies h . x is Function )
assume  x in dom h ; ::_thesis: h . x is Function
then  ex H being Function of (x \ (g . x)),(bool (x \ (g . x))) st
( h . x = H & H is one-to-one & rng H is with_non-empty_elements & rng H is c=-linear & dom H in rng H & ( for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) ) ) by A27;
hence  h . x is Function ; ::_thesis: verum
end;
then reconsider h = h as Function-yielding Function by FUNCOP_1:def_6;
deffunc H1( set ) ->  set = (g . (f . $1)) \/ ((h . (f . $1)) . $1);
A28: for x being set st x in X holds
x in (f . x) \ (g . (f . x))
proof
let x be set ; ::_thesis: ( x in X implies x in (f . x) \ (g . (f . x)) )
assume A29: x in X ; ::_thesis: x in (f . x) \ (g . (f . x))
then A30: f . x in Y by A7;
assume A31: not x in (f . x) \ (g . (f . x)) ; ::_thesis: contradiction
 x in f . x by A7, A29;
then A32: x in g . (f . x) by A31, XBOOLE_0:def_5;
then  g . (f . x) in Y by A20, A30;
then A33: f . x c= g . (f . x) by A7, A32;
 g . (f . x) c< f . x by A20, A30;
hence  contradiction by A33, XBOOLE_0:def_8; ::_thesis: verum
end;
A34: for x being set st x in X holds
H1(x) in bool X
proof
let x be set ; ::_thesis: ( x in X implies H1(x) in bool X )
set fx = f . x;
assume A35: x in X ; ::_thesis: H1(x) in bool X
then A36: f . x in Y by A7;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A37: h . (f . x) = H and
 H is one-to-one and
 ( rng H is with_non-empty_elements & rng H is c=-linear ) and
 dom H in rng H and
 for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
A38: x in (f . x) \ (g . (f . x)) by A28, A35;
 dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def_1;
then  H . x in rng H by A38, FUNCT_1:def_3;
then  H . x c= f . x by XBOOLE_1:1;
then A39: H . x c= X by A36, XBOOLE_1:1;
 ( g . (f . x) in Y or g . (f . x) is empty ) by A20, A36;
then  H1(x) c= X by A37, A39, XBOOLE_1:8;
hence  H1(x) in bool X ; ::_thesis: verum
end;
consider z being Function of X,(bool X) such that
A40: for x being set st x in X holds
z . x = H1(x) from FUNCT_2:sch_2(A34);
A41: dom z = X by FUNCT_2:def_1;
A42: Y c= rng z
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng z )
assume A43: y in Y ; ::_thesis: y in rng z
then consider H being Function of (y \ (g . y)),(bool (y \ (g . y))) such that
A44: h . y = H and
 H is one-to-one and
 ( rng H is with_non-empty_elements & rng H is c=-linear ) and
A45: dom H in rng H and
 for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
consider x being set  such that
A46: x in dom H and
A47: H . x = dom H by A45, FUNCT_1:def_3;
A48: dom H = y \ (g . y) by FUNCT_2:def_1;
then A49: x in y by A46;
then A50: x in f . x by A7, A43;
 g . y c< y by A20, A43;
then A51: g . y c= y by XBOOLE_0:def_8;
A52: f . x c= y by A7, A43, A49;
A53: f . x in Y by A7, A43, A49;
 f . x = y
proof
assume  f . x <> y ; ::_thesis: contradiction
then  f . x c< y by A52, XBOOLE_0:def_8;
then  f . x c= g . y by A20, A43, A53;
hence  contradiction by A46, A50, XBOOLE_0:def_5; ::_thesis: verum
end;
then z . x = (g . y) \/ (y \ (g . y)) by A40, A43, A44, A47, A48, A49
.= y by A51, XBOOLE_1:45 ;
hence  y in rng z by A41, A43, A49, FUNCT_1:def_3; ::_thesis: verum
end;
A54: for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z )
proof
let Z be set ; ::_thesis: ( Z in rng z & card Z <> 1 implies ex x being set st
( x in Z & Z \ {x} in rng z ) )
assume that
A55: Z in rng z and
A56: card Z <> 1 ; ::_thesis: ex x being set st
( x in Z & Z \ {x} in rng z )
consider x being set  such that
A57: x in dom z and
A58: z . x = Z by A55, FUNCT_1:def_3;
set fx = f . x;
A59: f . x in Y by A7, A57;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A60: h . (f . x) = H and
 H is one-to-one and
 ( rng H is with_non-empty_elements & rng H is c=-linear ) and
 dom H in rng H and
A61: for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
A62: z . x = (g . (f . x)) \/ (H . x) by A40, A57, A60;
A63: dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def_1;
 x in (f . x) \ (g . (f . x)) by A28, A57;
then A64: H . x in rng H by A63, FUNCT_1:def_3;
percases ( card (H . x) = 1 or card (H . x) <> 1 ) ;
supposeA65: card (H . x) = 1 ; ::_thesis: ex x being set st
( x in Z & Z \ {x} in rng z )
then  g . (f . x) <> {} by A56, A58, A62;
then A66: g . (f . x) in Y by A20, A59;
consider a being set  such that
A67: H . x = {a} by A65, CARD_2:42;
take  a ; ::_thesis: ( a in Z & Z \ {a} in rng z )
A68: a in H . x by A67, TARSKI:def_1;
then A69: not a in g . (f . x) by A64, XBOOLE_0:def_5;
thus  a in Z by A58, A62, A68, XBOOLE_0:def_3; ::_thesis: Z \ {a} in rng z
Z \ {a} = ((g . (f . x)) \/ (H . x)) \ (H . x) by A40, A57, A58, A60, A67
.= (g . (f . x)) \ (H . x) by XBOOLE_1:40
.= g . (f . x) by A67, A69, ZFMISC_1:57 ;
hence  Z \ {a} in rng z by A42, A66; ::_thesis: verum
end;
suppose card (H . x) <> 1 ; ::_thesis: ex x being set st
( x in Z & Z \ {x} in rng z )
then consider a being set  such that
A70: a in H . x and
A71: (H . x) \ {a} in rng H by A61, A64;
A72: not a in g . (f . x) by A64, A70, XBOOLE_0:def_5;
take  a ; ::_thesis: ( a in Z & Z \ {a} in rng z )
thus  a in Z by A58, A62, A70, XBOOLE_0:def_3; ::_thesis: Z \ {a} in rng z
consider b being set  such that
A73: b in dom H and
A74: H . b = (H . x) \ {a} by A71, FUNCT_1:def_3;
A75: b in f . x by A63, A73;
then A76: b in f . b by A7, A59;
A77: f . b in Y by A7, A59, A75;
A78: f . b c= f . x by A7, A59, A75;
 f . x = f . b
proof
assume  f . x <> f . b ; ::_thesis: contradiction
then  f . b c< f . x by A78, XBOOLE_0:def_8;
then  f . b c= g . (f . x) by A20, A59, A77;
hence  contradiction by A73, A76, XBOOLE_0:def_5; ::_thesis: verum
end;
then z . b = (g . (f . x)) \/ ((H . x) \ {a}) by A40, A59, A60, A74, A75
.= ((g . (f . x)) \/ (H . x)) \ {a} by A72, XBOOLE_1:87, ZFMISC_1:50
.= Z \ {a} by A58, A40, A57, A60 ;
hence  Z \ {a} in rng z by A41, A59, A75, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
A79: rng z is c=-linear
proof
let y1, y2 be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not y1 in rng z or not y2 in rng z or y1,y2 are_c=-comparable )
assume that
A80: y1 in rng z and
A81: y2 in rng z ; ::_thesis: y1,y2 are_c=-comparable
consider x1 being set  such that
A82: x1 in dom z and
A83: z . x1 = y1 by A80, FUNCT_1:def_3;
consider x2 being set  such that
A84: x2 in dom z and
A85: z . x2 = y2 by A81, FUNCT_1:def_3;
set fx1 = f . x1;
set fx2 = f . x2;
A86: x1 in (f . x1) \ (g . (f . x1)) by A28, A82;
A87: f . x1 in Y by A7, A82;
then consider H1 being Function of ((f . x1) \ (g . (f . x1))),(bool ((f . x1) \ (g . (f . x1)))) such that
A88: h . (f . x1) = H1 and
 H1 is one-to-one and
 ( rng H1 is with_non-empty_elements & rng H1 is c=-linear ) and
 dom H1 in rng H1 and
 for Z being set st Z in rng H1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H1 ) by A27;
A89: z . x1 = (g . (f . x1)) \/ (H1 . x1) by A40, A82, A88;
 dom H1 = (f . x1) \ (g . (f . x1)) by FUNCT_2:def_1;
then A90: H1 . x1 in rng H1 by A86, FUNCT_1:def_3;
A91: x2 in (f . x2) \ (g . (f . x2)) by A28, A84;
A92: f . x2 in Y by A7, A84;
then consider H2 being Function of ((f . x2) \ (g . (f . x2))),(bool ((f . x2) \ (g . (f . x2)))) such that
A93: h . (f . x2) = H2 and
 H2 is one-to-one and
A94: ( rng H2 is with_non-empty_elements & rng H2 is c=-linear ) and
 dom H2 in rng H2 and
 for Z being set st Z in rng H2 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H2 ) by A27;
A95: z . x2 = (g . (f . x2)) \/ (H2 . x2) by A40, A84, A93;
 dom H2 = (f . x2) \ (g . (f . x2)) by FUNCT_2:def_1;
then A96: H2 . x2 in rng H2 by A91, FUNCT_1:def_3;
A97: f . x1,f . x2 are_c=-comparable by A1, A87, A92, ORDINAL1:def_8;
percases ( f . x1 = f . x2 or ( f . x1 c= f . x2 & f . x1 <> f . x2 ) or ( f . x2 c= f . x1 & f . x1 <> f . x2 ) ) by A97, XBOOLE_0:def_9;
supposeA98: f . x1 = f . x2 ; ::_thesis: y1,y2 are_c=-comparable
then  H1 . x1,H1 . x2 are_c=-comparable by A88, A90, A93, A94, A96, ORDINAL1:def_8;
then  ( H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x1 ) by XBOOLE_0:def_9;
then  ( z . x1 c= z . x2 or z . x2 c= z . x1 ) by A88, A89, A93, A95, A98, XBOOLE_1:9;
hence  y1,y2 are_c=-comparable by A83, A85, XBOOLE_0:def_9; ::_thesis: verum
end;
suppose ( f . x1 c= f . x2 & f . x1 <> f . x2 ) ; ::_thesis: y1,y2 are_c=-comparable
then  f . x1 c< f . x2 by XBOOLE_0:def_8;
then A99: f . x1 c= g . (f . x2) by A20, A87, A92;
 g . (f . x2) c= z . x2 by A95, XBOOLE_1:7;
then A100: f . x1 c= z . x2 by A99, XBOOLE_1:1;
 g . (f . x1) c< f . x1 by A20, A87;
then  g . (f . x1) c= f . x1 by XBOOLE_0:def_8;
then A101: (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1 by XBOOLE_1:45;
 z . x1 c= (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) by A89, A90, XBOOLE_1:9;
then  z . x1 c= z . x2 by A100, A101, XBOOLE_1:1;
hence  y1,y2 are_c=-comparable by A83, A85, XBOOLE_0:def_9; ::_thesis: verum
end;
suppose ( f . x2 c= f . x1 & f . x1 <> f . x2 ) ; ::_thesis: y1,y2 are_c=-comparable
then  f . x2 c< f . x1 by XBOOLE_0:def_8;
then A102: f . x2 c= g . (f . x1) by A20, A87, A92;
 g . (f . x1) c= z . x1 by A89, XBOOLE_1:7;
then A103: f . x2 c= z . x1 by A102, XBOOLE_1:1;
 g . (f . x2) c< f . x2 by A20, A92;
then  g . (f . x2) c= f . x2 by XBOOLE_0:def_8;
then A104: (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2 by XBOOLE_1:45;
 z . x2 c= (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) by A95, A96, XBOOLE_1:9;
then  z . x2 c= z . x1 by A103, A104, XBOOLE_1:1;
hence  y1,y2 are_c=-comparable by A83, A85, XBOOLE_0:def_9; ::_thesis: verum
end;
end;
end;
A105: rng z is with_non-empty_elements
proof
assume  not rng z is with_non-empty_elements ; ::_thesis: contradiction
then  {} in rng z by SETFAM_1:def_8;
then consider x being set  such that
A106: x in dom z and
A107: z . x = {} by FUNCT_1:def_3;
set fx = f . x;
A108: x in (f . x) \ (g . (f . x)) by A28, A106;
 f . x in Y by A7, A106;
then consider H being Function of ((f . x) \ (g . (f . x))),(bool ((f . x) \ (g . (f . x)))) such that
A109: h . (f . x) = H and
 H is one-to-one and
A110: ( rng H is with_non-empty_elements & rng H is c=-linear ) and
 dom H in rng H and
 for Z being set st Z in rng H & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H ) by A27;
 dom H = (f . x) \ (g . (f . x)) by FUNCT_2:def_1;
then A111: H . x in rng H by A108, FUNCT_1:def_3;
 z . x = (g . (f . x)) \/ (H . x) by A40, A106, A109;
hence  contradiction by A107, A110, A111; ::_thesis: verum
end;
take  rng z ; ::_thesis: ( Y c= rng z & rng z is with_non-empty_elements & rng z is c=-linear & card X = card (rng z) & ( for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z ) ) )
 for x1, x2 being set st x1 in dom z & x2 in dom z & z . x1 = z . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom z & x2 in dom z & z . x1 = z . x2 implies x1 = x2 )
set f1 = f . x1;
set f2 = f . x2;
assume that
A112: x1 in dom z and
A113: x2 in dom z and
A114: z . x1 = z . x2 ; ::_thesis: x1 = x2
A115: ( z . x1 = H1(x1) & z . x2 = H1(x2) ) by A40, A112, A113;
A116: f . x2 in Y by A7, A113;
then consider H2 being Function of ((f . x2) \ (g . (f . x2))),(bool ((f . x2) \ (g . (f . x2)))) such that
A117: h . (f . x2) = H2 and
A118: H2 is one-to-one and
A119: ( rng H2 is with_non-empty_elements & rng H2 is c=-linear ) and
 dom H2 in rng H2 and
 for Z being set st Z in rng H2 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H2 ) by A27;
 dom H2 = (f . x2) \ (g . (f . x2)) by FUNCT_2:def_1;
then A120: x2 in dom H2 by A28, A113;
then A121: H2 . x2 in rng H2 by FUNCT_1:def_3;
then A122: g . (f . x2) misses H2 . x2 by XBOOLE_1:63, XBOOLE_1:79;
A123: f . x1 in Y by A7, A112;
then consider H1 being Function of ((f . x1) \ (g . (f . x1))),(bool ((f . x1) \ (g . (f . x1)))) such that
A124: h . (f . x1) = H1 and
 H1 is one-to-one and
A125: ( rng H1 is with_non-empty_elements & rng H1 is c=-linear ) and
 dom H1 in rng H1 and
 for Z being set st Z in rng H1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng H1 ) by A27;
 dom H1 = (f . x1) \ (g . (f . x1)) by FUNCT_2:def_1;
then A126: x1 in dom H1 by A28, A112;
then A127: H1 . x1 in rng H1 by FUNCT_1:def_3;
then A128: g . (f . x1) misses H1 . x1 by XBOOLE_1:63, XBOOLE_1:79;
A129: f . x1,f . x2 are_c=-comparable by A1, A116, A123, ORDINAL1:def_8;
percases ( f . x1 = f . x2 or ( f . x1 c= f . x2 & f . x1 <> f . x2 ) or ( f . x2 c= f . x1 & f . x1 <> f . x2 ) ) by A129, XBOOLE_0:def_9;
supposeA130: f . x1 = f . x2 ; ::_thesis: x1 = x2
then  H1 . x1 = H1 . x2 by A114, A115, A117, A122, A124, A128, XBOOLE_1:71;
hence  x1 = x2 by A117, A118, A120, A124, A126, A130, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA131: ( f . x1 c= f . x2 & f . x1 <> f . x2 ) ; ::_thesis: x1 = x2
 g . (f . x1) c< f . x1 by A20, A123;
then  g . (f . x1) c= f . x1 by XBOOLE_0:def_8;
then  (g . (f . x1)) \/ ((f . x1) \ (g . (f . x1))) = f . x1 by XBOOLE_1:45;
then A132: H1(x2) c= f . x1 by A114, A115, A124, A127, XBOOLE_1:9;
 f . x1 c< f . x2 by A131, XBOOLE_0:def_8;
then  f . x1 c= g . (f . x2) by A20, A116, A123;
then  H1(x2) c= g . (f . x2) by A132, XBOOLE_1:1;
then  H2 . x2 c= g . (f . x2) by A117, XBOOLE_1:11;
hence  x1 = x2 by A119, A121, XBOOLE_1:67, XBOOLE_1:79; ::_thesis: verum
end;
supposeA133: ( f . x2 c= f . x1 & f . x1 <> f . x2 ) ; ::_thesis: x1 = x2
 g . (f . x2) c< f . x2 by A20, A116;
then  g . (f . x2) c= f . x2 by XBOOLE_0:def_8;
then  (g . (f . x2)) \/ ((f . x2) \ (g . (f . x2))) = f . x2 by XBOOLE_1:45;
then A134: H1(x1) c= f . x2 by A114, A115, A117, A121, XBOOLE_1:9;
 f . x2 c< f . x1 by A133, XBOOLE_0:def_8;
then  f . x2 c= g . (f . x1) by A20, A116, A123;
then  H1(x1) c= g . (f . x1) by A134, XBOOLE_1:1;
then  H1 . x1 c= g . (f . x1) by A124, XBOOLE_1:11;
hence  x1 = x2 by A125, A127, XBOOLE_1:67, XBOOLE_1:79; ::_thesis: verum
end;
end;
end;
then  z is one-to-one by FUNCT_1:def_4;
then  X, rng z are_equipotent by A41, WELLORD2:def_4;
hence  ( Y c= rng z & rng z is with_non-empty_elements & rng z is c=-linear & card X = card (rng z) & ( for Z being set st Z in rng z & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in rng z ) ) ) by A42, A54, A79, A105, CARD_1:5; ::_thesis: verum
end;

begin

definition
mode SimplicialComplexStr is TopStruct ;
end;

notation
let K be SimplicialComplexStr;
let A be Subset of K;
synonym  simplex-like A for  open ;
end;

notation
let K be SimplicialComplexStr;
let S be Subset-Family of K;
synonym  simplex-like S for  open ;
end;

registration
let K be SimplicialComplexStr;
cluster empty simplex-like for Element of bool (bool the carrier of K);
existence
 ex b1 being Subset-Family of K st
( b1 is empty & b1 is simplex-like )
proof
take E = {} (bool the carrier of K); ::_thesis: ( E is empty & E is simplex-like )
 for A being Subset of K st A in E holds
A is open ;
hence  ( E is empty & E is simplex-like ) by TOPS_2:def_1; ::_thesis: verum
end;
end;

theorem Th14: :: SIMPLEX0:14
for K being SimplicialComplexStr
for S being Subset-Family of K holds
( S is simplex-like iff S c= the topology of K )
proof
let K be SimplicialComplexStr; ::_thesis: for S being Subset-Family of K holds
( S is simplex-like iff S c= the topology of K )
let S be Subset-Family of K; ::_thesis: ( S is simplex-like iff S c= the topology of K )
hereby  ::_thesis: ( S c= the topology of K implies S is simplex-like )
assume A1: S is simplex-like ; ::_thesis: S c= the topology of K
thus  S c= the topology of K ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the topology of K )
assume A2: x in S ; ::_thesis: x in the topology of K
then reconsider A = x as Subset of K ;
 A is simplex-like by A1, A2, TOPS_2:def_1;
hence  x in the topology of K by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
assume A3: S c= the topology of K ; ::_thesis: S is simplex-like
let A be Subset of K; :: according to TOPS_2:def_1 ::_thesis: ( not A in S or A is simplex-like )
assume  A in S ; ::_thesis: A is simplex-like
hence  A is simplex-like by A3, PRE_TOPC:def_2; ::_thesis: verum
end;

definition
let K be SimplicialComplexStr;
let v be Element of K;
attrv is vertex-like  means :Def3: :: SIMPLEX0:def 3
 ex S being Subset of K st
( S is simplex-like & v in S );
end;

:: deftheorem Def3 defines vertex-like SIMPLEX0:def_3_:_
 for K being SimplicialComplexStr
for v being Element of K holds
( v is vertex-like iff ex S being Subset of K st
( S is simplex-like & v in S ) );

definition
let K be SimplicialComplexStr;
func Vertices K ->  Subset of K means :Def4: :: SIMPLEX0:def 4
 for v being Element of K holds
( v in it iff v is vertex-like );
existence
 ex b1 being Subset of K st
for v being Element of K holds
( v in b1 iff v is vertex-like )
proof
set B =  {  v where v is Element of K : v is vertex-like  }  ;
  {  v where v is Element of K : v is vertex-like  }  c= [#] K
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Element of K : v is vertex-like  }  or x in [#] K )
assume  x in  {  v where v is Element of K : v is vertex-like  }  ; ::_thesis: x in [#] K
then consider v being Element of K such that
A1: x = v and
A2: v is vertex-like ;
 ex S being Subset of K st
( S is simplex-like & v in S ) by A2, Def3;
hence  x in [#] K by A1; ::_thesis: verum
end;
then reconsider B =  {  v where v is Element of K : v is vertex-like  }  as Subset of K ;
take  B ; ::_thesis: for v being Element of K holds
( v in B iff v is vertex-like )
let v be Element of K; ::_thesis: ( v in B iff v is vertex-like )
hereby  ::_thesis: ( v is vertex-like implies v in B )
assume  v in B ; ::_thesis: v is vertex-like
then  ex w being Element of K st
( v = w & w is vertex-like ) ;
hence  v is vertex-like ; ::_thesis: verum
end;
assume  v is vertex-like ; ::_thesis: v in B
hence  v in B ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of K st ( for v being Element of K holds
( v in b1 iff v is vertex-like ) ) & ( for v being Element of K holds
( v in b2 iff v is vertex-like ) ) holds
b1 = b2
proof
let V1, V2 be Subset of K; ::_thesis: ( ( for v being Element of K holds
( v in V1 iff v is vertex-like ) ) & ( for v being Element of K holds
( v in V2 iff v is vertex-like ) ) implies V1 = V2 )
assume that
A3: for v being Element of K holds
( v in V1 iff v is vertex-like ) and
A4: for v being Element of K holds
( v in V2 iff v is vertex-like ) ; ::_thesis: V1 = V2
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: V2 c= V1
let x be set ; ::_thesis: ( x in V1 implies x in V2 )
assume A5: x in V1 ; ::_thesis: x in V2
then reconsider v = x as Element of K ;
 v is vertex-like by A3, A5;
hence  x in V2 by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V2 or x in V1 )
assume A6: x in V2 ; ::_thesis: x in V1
then reconsider v = x as Element of K ;
 v is vertex-like by A4, A6;
hence  x in V1 by A3; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Vertices SIMPLEX0:def_4_:_
 for K being SimplicialComplexStr
for b2 being Subset of K holds
( b2 = Vertices K iff for v being Element of K holds
( v in b2 iff v is vertex-like ) );

definition
let K be SimplicialComplexStr;
mode Vertex of K is Element of Vertices K;
end;

definition
let K be SimplicialComplexStr;
attrK is finite-vertices  means :Def5: :: SIMPLEX0:def 5
 Vertices K is finite ;
end;

:: deftheorem Def5 defines finite-vertices SIMPLEX0:def_5_:_
 for K being SimplicialComplexStr holds
( K is finite-vertices iff Vertices K is finite );

definition
let K be SimplicialComplexStr;
attrK is locally-finite  means :Def6: :: SIMPLEX0:def 6
 for v being Vertex of K holds  {  S where S is Subset of K : ( S is simplex-like & v in S )  }  is finite ;
end;

:: deftheorem Def6 defines locally-finite SIMPLEX0:def_6_:_
 for K being SimplicialComplexStr holds
( K is locally-finite iff for v being Vertex of K holds  {  S where S is Subset of K : ( S is simplex-like & v in S )  }  is finite );

definition
let K be SimplicialComplexStr;
attrK is empty-membered  means :Def7: :: SIMPLEX0:def 7
 the topology of K is empty-membered ;
attrK is with_non-empty_elements  means :Def8: :: SIMPLEX0:def 8
 the topology of K is with_non-empty_elements ;
end;

:: deftheorem Def7 defines empty-membered SIMPLEX0:def_7_:_
 for K being SimplicialComplexStr holds
( K is empty-membered iff the topology of K is empty-membered );

:: deftheorem Def8 defines with_non-empty_elements SIMPLEX0:def_8_:_
 for K being SimplicialComplexStr holds
( K is with_non-empty_elements iff the topology of K is with_non-empty_elements );

notation
let K be SimplicialComplexStr;
antonym  with_non-empty_element K for  empty-membered ;
antonym  with_empty_element K for  with_non-empty_elements ;
end;

definition
let X be set ;
mode SimplicialComplexStr of X ->  SimplicialComplexStr means :Def9: :: SIMPLEX0:def 9
 [#] it c= X;
existence
 ex b1 being SimplicialComplexStr st [#] b1 c= X
proof
take  the empty TopStruct ; ::_thesis: [#] the empty TopStruct c= X
thus  [#] the empty TopStruct c= X by XBOOLE_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines SimplicialComplexStr SIMPLEX0:def_9_:_
 for X being set
for b2 being SimplicialComplexStr holds
( b2 is SimplicialComplexStr of X iff [#] b2 c= X );

definition
let X be set ;
let KX be SimplicialComplexStr of X;
attrKX is total  means :Def10: :: SIMPLEX0:def 10
 [#] KX = X;
end;

:: deftheorem Def10 defines total SIMPLEX0:def_10_:_
 for X being set
for KX being SimplicialComplexStr of X holds
( KX is total iff [#] KX = X );

Lm2:  for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered )
proof
let K be SimplicialComplexStr; ::_thesis: ( Vertices K is empty iff K is empty-membered )
hereby  ::_thesis: ( K is empty-membered implies Vertices K is empty )
assume A1: Vertices K is empty ; ::_thesis: not K is with_non-empty_element
assume  K is with_non-empty_element ; ::_thesis: contradiction
then  the topology of K is with_non-empty_element by Def7;
then consider D being non empty set  such that
A2: D in the topology of K by SETFAM_1:def_10;
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, PRE_TOPC:def_2;
then  v is vertex-like by Def3;
hence  contradiction by A1, Def4; ::_thesis: verum
end;
assume A3: K is empty-membered ; ::_thesis: Vertices K is empty
assume  not Vertices K is empty ; ::_thesis: contradiction
then consider x being set  such that
A4: x in Vertices K by XBOOLE_0:def_1;
reconsider x = x as Element of K by A4;
 x is vertex-like by A4, Def4;
then consider S being Subset of K such that
A5: S is simplex-like and
A6: x in S by Def3;
 S in the topology of K by A5, PRE_TOPC:def_2;
then  the topology of K is with_non-empty_element by A6, SETFAM_1:def_10;
hence  contradiction by A3, Def7; ::_thesis: verum
end;

Lm3:  for x being set
for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
proof
let x be set ; ::_thesis: for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
let K be SimplicialComplexStr; ::_thesis: for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
let S be Subset of K; ::_thesis: ( S is simplex-like & x in S implies x in Vertices K )
assume that
A1: S is simplex-like and
A2: x in S ; ::_thesis: x in Vertices K
reconsider v = x as Element of K by A2;
 v is vertex-like by A1, A2, Def3;
hence  x in Vertices K by Def4; ::_thesis: verum
end;

Lm4:  for K being SimplicialComplexStr
for A being Subset of K st A is simplex-like holds
A c= Vertices K
proof
let K be SimplicialComplexStr; ::_thesis: for A being Subset of K st A is simplex-like holds
A c= Vertices K
let A be Subset of K; ::_thesis: ( A is simplex-like implies A c= Vertices K )
assume A1: A is simplex-like ; ::_thesis: A c= Vertices K
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Vertices K )
thus  ( not x in A or x in Vertices K ) by A1, Lm3; ::_thesis: verum
end;

Lm5:  for K being SimplicialComplexStr holds Vertices K = union the topology of K
proof
let K be SimplicialComplexStr; ::_thesis: Vertices K = union the topology of K
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union the topology of K c= Vertices K
let x be set ; ::_thesis: ( x in Vertices K implies x in union the topology of K )
assume A1: x in Vertices K ; ::_thesis: x in union the topology of K
reconsider v = x as Element of K by A1;
 v is vertex-like by A1, Def4;
then consider S being Subset of K such that
A2: S is simplex-like and
A3: v in S by Def3;
 S in the topology of K by A2, PRE_TOPC:def_2;
hence  x in union the topology of K by A3, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union the topology of K or x in Vertices K )
assume  x in union the topology of K ; ::_thesis: x in Vertices K
then consider y being set  such that
A4: x in y and
A5: y in the topology of K by TARSKI:def_4;
reconsider y = y as Subset of K by A5;
 y is simplex-like by A5, PRE_TOPC:def_2;
hence  x in Vertices K by A4, Lm3; ::_thesis: verum
end;

Lm6:  for K being SimplicialComplexStr st K is finite-vertices holds
the topology of K is finite
proof
let K be SimplicialComplexStr; ::_thesis: ( K is finite-vertices implies the topology of K is finite )
 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 ; ::_thesis: the topology of K is finite
then  Vertices K is finite by Def5;
hence  the topology of K is finite by A1; ::_thesis: verum
end;

registration
cluster with_empty_element  ->  non void for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st b1 is with_empty_element holds
not b1 is void
proof
let K be SimplicialComplexStr; ::_thesis: ( K is with_empty_element implies not K is void )
assume  K is with_empty_element ; ::_thesis: not K is void
then  the topology of K is with_empty_element by Def8;
hence  not K is void by PENCIL_1:def_4; ::_thesis: verum
end;
cluster with_non-empty_element  ->  non void for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st b1 is with_non-empty_element holds
not b1 is void
proof
let K be SimplicialComplexStr; ::_thesis: ( K is with_non-empty_element implies not K is void )
assume  K is with_non-empty_element ; ::_thesis: not K is void
then  the topology of K is with_non-empty_element by Def7;
hence  not K is void by PENCIL_1:def_4; ::_thesis: verum
end;
cluster non void empty-membered  ->  with_empty_element for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st not b1 is void & b1 is empty-membered holds
b1 is with_empty_element
proof
let K be SimplicialComplexStr; ::_thesis: ( not K is void & K is empty-membered implies K is with_empty_element )
assume  ( not K is void & K is empty-membered ) ; ::_thesis: K is with_empty_element
then  the topology of K is with_empty_element by Def7;
hence  K is with_empty_element by Def8; ::_thesis: verum
end;
cluster non void subset-closed  ->  with_empty_element for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st not b1 is void & b1 is subset-closed holds
b1 is with_empty_element
proof
let K be SimplicialComplexStr; ::_thesis: ( not K is void & K is subset-closed implies K is with_empty_element )
assume A1: ( not K is void & K is subset-closed ) ; ::_thesis: K is with_empty_element
then  ex x being set st x in the_family_of K by XBOOLE_0:def_1;
hence  K is with_empty_element by A1, Def8; ::_thesis: verum
end;
cluster empty-membered  ->  subset-closed finite-vertices for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st b1 is empty-membered holds
( b1 is subset-closed & b1 is finite-vertices )
proof
let K be SimplicialComplexStr; ::_thesis: ( K is empty-membered implies ( K is subset-closed & K is finite-vertices ) )
assume A2: K is empty-membered ; ::_thesis: ( K is subset-closed & K is finite-vertices )
then A3: the topology of K is empty-membered by Def7;
thus  K is subset-closed ::_thesis: K is finite-vertices
proof
let x be set ; :: according to CLASSES1:def_1,MATROID0:def_3 ::_thesis: for b1 being set holds
( not x in the_family_of K or not b1 c= x or b1 in the_family_of K )
let y be set ; ::_thesis: ( not x in the_family_of K or not y c= x or y in the_family_of K )
assume that
A4: x in the_family_of K and
A5: y c= x ; ::_thesis: y in the_family_of K
 x is empty by A3, A4, SETFAM_1:def_10;
hence  y in the_family_of K by A4, A5; ::_thesis: verum
end;
 Vertices K is empty by A2, Lm2;
hence  K is finite-vertices by Def5; ::_thesis: verum
end;
cluster finite-vertices  ->  finite-degree locally-finite for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st b1 is finite-vertices holds
( b1 is locally-finite & b1 is finite-degree )
proof
let K be SimplicialComplexStr; ::_thesis: ( K is finite-vertices implies ( K is locally-finite & K is finite-degree ) )
assume A6: K is finite-vertices ; ::_thesis: ( K is locally-finite & K is finite-degree )
then reconsider V = Vertices K as finite Subset of K by Def5;
thus  K is locally-finite ::_thesis: K is finite-degree
proof
let v be Vertex of K; :: according to SIMPLEX0:def_6 ::_thesis:  {  S where S is Subset of K : ( S is simplex-like & v in S )  }  is finite
A7:  {  S where S is Subset of K : ( S is simplex-like & v in S )  }  c= the topology of K
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  S where S is Subset of K : ( S is simplex-like & v in S )  }  or x in the topology of K )
assume  x in  {  S where S is Subset of K : ( S is simplex-like & v in S )  }  ; ::_thesis: x in the topology of K
then  ex S being Subset of K st
( x = S & S is simplex-like & v in S ) ;
hence  x in the topology of K by PRE_TOPC:def_2; ::_thesis: verum
end;
 the topology of K is finite by A6, Lm6;
hence   {  S where S is Subset of K : ( S is simplex-like & v in S )  }  is finite by A7; ::_thesis: verum
end;
thus  K is finite-membered :: according to MATROID0:def_7 ::_thesis: ex b1 being set st
for b2 being Element of bool the carrier of K holds
( not b2 is simplex-like or card b2 <= b1 )
proof
let x be set ; :: according to FINSET_1:def_6,MATROID0:def_6 ::_thesis: ( not x in the_family_of K or x is finite )
assume A8: x in the_family_of K ; ::_thesis: x is finite
then reconsider X = x as Subset of K ;
 X is simplex-like by A8, PRE_TOPC:def_2;
then  X c= V by Lm4;
hence  x is finite ; ::_thesis: verum
end;
take  card V ; ::_thesis: for b1 being Element of bool the carrier of K holds
( not b1 is simplex-like or card b1 <= card V )
let A be finite Subset of K; ::_thesis: ( not A is simplex-like or card A <= card V )
assume  A is open ; ::_thesis: card A <= card V
hence  card A <= card V by Lm4, NAT_1:43; ::_thesis: verum
end;
cluster subset-closed locally-finite  ->  finite-membered for TopStruct ;
coherence
 for b1 being SimplicialComplexStr st b1 is locally-finite & b1 is subset-closed holds
b1 is finite-membered
proof
let K be SimplicialComplexStr; ::_thesis: ( K is locally-finite & K is subset-closed implies K is finite-membered )
assume A9: ( K is locally-finite & K is subset-closed ) ; ::_thesis: K is finite-membered
 the_family_of K is finite-membered
proof
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( not x in the_family_of K or x is finite )
assume A10: x in the_family_of K ; ::_thesis: x is finite
then reconsider A = x as Subset of K ;
A11: not K is void by A10, PENCIL_1:def_4;
A12: A is simplex-like by A10, PRE_TOPC:def_2;
percases ( x is empty or not x is empty ) ;
suppose x is empty ; ::_thesis: x is finite
hence  x is finite ; ::_thesis: verum
end;
suppose not x is empty ; ::_thesis: x is finite
then consider a being set  such that
A13: a in A by XBOOLE_0:def_1;
reconsider a = a as Element of K by A13;
 a is vertex-like by A12, A13, Def3;
then reconsider a = a as Vertex of K by Def4;
set Aa = A \ {a};
set X =  {  S where S is Subset of K : ( a in S & S c= A )  }  ;
defpred S1[ set , set ] means c1 \ {a} = c2;
set Z =  {  y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S1[w,y] & w in  {  S where S is Subset of K : ( a in S & S c= A )  }  )  }  ;
A14: bool (A \ {a}) c=  {  y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S1[w,y] & w in  {  S where S is Subset of K : ( a in S & S c= A )  }  )  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in bool (A \ {a}) or y in  {  y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S1[w,y] & w in  {  S where S is Subset of K : ( a in S & S c= A )  }  )  }  )
assume A15: y in bool (A \ {a}) ; ::_thesis: y in  {  y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S1[w,y] & w in  {  S where S is Subset of K : ( a in S & S c= A )  }  )  }
then reconsider B = y as Subset of K by XBOOLE_1:1;
 not a in B by A15, ZFMISC_1:56;
then A16: (B \/ {a}) \ {a} = B by ZFMISC_1:117;
A17: {a} c= A by A13, ZFMISC_1:31;
 A \ {a} c= A by XBOOLE_1:36;
then  y c= A by A15, XBOOLE_1:1;
then A18: B \/ {a} c= A by A17, XBOOLE_1:8;
then A19: 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  {  S where S is Subset of K : ( a in S & S c= A )  }  by A18, A19;
hence  y in  {  y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S1[w,y] & w in  {  S where S is Subset of K : ( a in S & S c= A )  }  )  }  by A15, A16, A19; ::_thesis: verum
end;
set Y =  {  S where S is Subset of K : ( S is simplex-like & a in S )  }  ;
A20:  {  S where S is Subset of K : ( a in S & S c= A )  }  c=  {  S where S is Subset of K : ( S is simplex-like & a in S )  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  S where S is Subset of K : ( a in S & S c= A )  }  or y in  {  S where S is Subset of K : ( S is simplex-like & a in S )  }  )
assume  y in  {  S where S is Subset of K : ( a in S & S c= A )  }  ; ::_thesis: y in  {  S where S is Subset of K : ( S is simplex-like & a in S )  }
then consider S being Subset of K such that
A21: ( y = S & a in S ) and
A22: S c= A ;
 S is simplex-like by A9, A11, A12, A22, MATROID0:1;
hence  y in  {  S where S is Subset of K : ( S is simplex-like & a in S )  }  by A21; ::_thesis: verum
end;
  {  S where S is Subset of K : ( S is simplex-like & a in S )  }  is finite by A9, Def6;
then A23:  {  S where S is Subset of K : ( a in S & S c= A )  }  is finite by A20;
A24: for w being Subset of K
for x, y being Element of bool (A \ {a}) st S1[w,x] & S1[w,y] holds
x = y ;
  {  y where y is Element of bool (A \ {a}) : ex w being Subset of K st
( S1[w,y] & w in  {  S where S is Subset of K : ( a in S & S c= A )  }  )  }  is finite from FRAENKEL:sch_28(A23, A24);
then A25: A \ {a} is finite by A14;
 A = (A \ {a}) \/ {a} by A13, ZFMISC_1:116;
hence  x is finite by A25; ::_thesis: verum
end;
end;
end;
hence  K is finite-membered by MATROID0:def_6; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster empty strict void empty-membered for SimplicialComplexStr of X;
existence
 ex b1 being SimplicialComplexStr of X st
( b1 is empty & b1 is void & b1 is empty-membered & b1 is strict )
proof
 [#] TopStruct(# {},({} (bool {})) #) c= X by XBOOLE_1:2;
then reconsider T = TopStruct(# {},({} (bool {})) #) as SimplicialComplexStr of X by Def9;
take  T ; ::_thesis: ( T is empty & T is void & T is empty-membered & T is strict )
thus  ( T is empty & T is void & T is empty-membered & T is strict ) ; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
cluster non empty strict non void empty-membered total for SimplicialComplexStr of D;
existence
 ex b1 being SimplicialComplexStr of D st
( not b1 is empty & not b1 is void & b1 is total & b1 is empty-membered & b1 is strict )
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 ; ::_thesis: ( not T is empty & not T is void & T is total & T is empty-membered & T is strict )
 for x being non empty set holds not x in B ;
then  ( [#] T = D & B is empty-membered ) by SETFAM_1:def_10;
hence  ( not T is empty & not T is void & T is total & T is empty-membered & T is strict ) by Def7, Def10, PENCIL_1:def_4; ::_thesis: verum
end;
cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element total for SimplicialComplexStr of D;
existence
 ex b1 being SimplicialComplexStr of D st
( not b1 is empty & b1 is total & b1 is with_empty_element & b1 is with_non-empty_element & b1 is finite-vertices & b1 is subset-closed & b1 is strict )
proof
set E = the Element of D;
reconsider B = bool { the Element of D} 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 ; ::_thesis: ( not T is empty & T is total & T is with_empty_element & T is with_non-empty_element & T is finite-vertices & T is subset-closed & T is strict )
A1: Vertices T c= { the Element of D}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Vertices T or x in { the Element of D} )
assume A2: x in Vertices T ; ::_thesis: x in { the Element of D}
reconsider v = x as Element of T by A2;
 v is vertex-like by A2, Def4;
then consider S being Subset of T such that
A3: S is simplex-like and
A4: v in S by Def3;
 S in B by A3, PRE_TOPC:def_2;
hence  x in { the Element of D} by A4; ::_thesis: verum
end;
 { the Element of D} in B by ZFMISC_1:def_1;
then  B is with_non-empty_element by SETFAM_1:def_10;
then A5: ( [#] T = D & T is with_non-empty_element ) by Def7;
 B = the_family_of T ;
then  T is subset-closed by MATROID0:def_3;
hence  ( not T is empty & T is total & T is with_empty_element & T is with_non-empty_element & T is finite-vertices & T is subset-closed & T is strict ) by A1, A5, Def5, Def10; ::_thesis: verum
end;
end;

registration
cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element for TopStruct ;
existence
 ex b1 being SimplicialComplexStr st
( not b1 is empty & b1 is with_empty_element & b1 is with_non-empty_element & b1 is finite-vertices & b1 is subset-closed & b1 is strict )
proof
take  the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set ; ::_thesis: ( not the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is empty & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is with_empty_element & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is with_non-empty_element & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is finite-vertices & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is subset-closed & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is strict )
thus  ( not the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is empty & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is with_empty_element & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is with_non-empty_element & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is finite-vertices & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is subset-closed & the non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element SimplicialComplexStr of the non empty set is strict ) ; ::_thesis: verum
end;
end;

registration
let K be with_non-empty_element SimplicialComplexStr;
cluster Vertices K ->  non empty ;
coherence
 not Vertices K is empty by Lm2;
end;

registration
let K be finite-vertices SimplicialComplexStr;
cluster simplex-like  ->  finite for Element of bool (bool the carrier of K);
coherence
 for b1 being Subset-Family of K st b1 is simplex-like holds
b1 is finite
proof
let S be Subset-Family of K; ::_thesis: ( S is simplex-like implies S is finite )
assume  S is simplex-like ; ::_thesis: S is finite
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  S is finite by A1, A2; ::_thesis: verum
end;
end;

registration
let K be finite-membered SimplicialComplexStr;
cluster simplex-like  ->  finite-membered for Element of bool (bool the carrier of K);
coherence
 for b1 being Subset-Family of K st b1 is simplex-like holds
b1 is finite-membered
proof
let S be Subset-Family of K; ::_thesis: ( S is simplex-like implies S is finite-membered )
assume A1: S is simplex-like ; ::_thesis: S is finite-membered
let x be set ; :: according to FINSET_1:def_6 ::_thesis: ( not x in S or x is finite )
assume A2: x in S ; ::_thesis: x is finite
then reconsider X = x as Subset of K ;
 X is simplex-like by A1, A2, TOPS_2:def_1;
then A3: X in the topology of K by PRE_TOPC:def_2;
 the_family_of K is finite-membered by MATROID0:def_6;
hence  x is finite by A3; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:15
for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered ) by Lm2;

theorem :: SIMPLEX0:16
for K being SimplicialComplexStr holds Vertices K = union the topology of K by Lm5;

theorem :: SIMPLEX0:17
for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like holds
S c= Vertices K by Lm4;

theorem :: SIMPLEX0:18
for K being SimplicialComplexStr st K is finite-vertices holds
the topology of K is finite by Lm6;

theorem Th19: :: SIMPLEX0:19
for K being SimplicialComplexStr st the topology of K is finite & not K is finite-vertices holds
not K is finite-membered
proof
let K be SimplicialComplexStr; ::_thesis: ( the topology of K is finite & not K is finite-vertices implies not K is finite-membered )
defpred S1[ set , set ] means $1 in $2;
set V = Vertices K;
assume that
A1: the topology of K is finite and
A2: not K is finite-vertices ; ::_thesis: not K is finite-membered
A3: Vertices K is infinite by A2, Def5;
A4: Vertices K = union the topology of K by Lm5;
A5: for x being set st x in Vertices K holds
ex y being set st
( y in the topology of K & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Vertices K implies ex y being set st
( y in the topology of K & S1[x,y] ) )
assume  x in Vertices K ; ::_thesis: ex y being set st
( y in the topology of K & S1[x,y] )
then  ex y being set st
( x in y & y in the topology of K ) by A4, TARSKI:def_4;
hence  ex y being set st
( y in the topology of K & S1[x,y] ) ; ::_thesis: verum
end;
consider f being Function of (Vertices K), the topology of K such that
A6: for x being set st x in Vertices K holds
S1[x,f . x] from FUNCT_2:sch_1(A5);
 not the topology of K is empty by A2, A4, Def5;
then  dom f = Vertices K by FUNCT_2:def_1;
then consider x being set  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 = x as Subset of K ;
 f " {x} c= x
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " {x} or y in x )
assume  y in f " {x} ; ::_thesis: y in x
then  ( f . y in {x} & y in f . y ) by A6, FUNCT_1:def_7;
hence  y in x by TARSKI:def_1; ::_thesis: verum
end;
then  not x is finite by A8;
then  not the_family_of K is finite-membered by A7;
hence  not K is finite-membered by MATROID0:def_6; ::_thesis: verum
end;

theorem Th20: :: SIMPLEX0:20
for K being SimplicialComplexStr st K is subset-closed & the topology of K is finite holds
K is finite-vertices
proof
let K be SimplicialComplexStr; ::_thesis: ( K is subset-closed & the topology of K is finite implies K is finite-vertices )
assume that
A1: K is subset-closed and
A2: the topology of K is finite ; ::_thesis: K is finite-vertices
assume  not K is finite-vertices ; ::_thesis: contradiction
then  not K is finite-membered by A2, Th19;
then  not the_family_of K is finite-membered by MATROID0:def_6;
then consider x being set  such that
A3: x in the_family_of K and
A4: not x is finite by FINSET_1:def_6;
 {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; ::_thesis: verum
end;

begin

definition
let X be set ;
let Y be Subset-Family of X;
func Complex_of Y ->  strict SimplicialComplexStr of X equals :: SIMPLEX0:def 11
 TopStruct(# X,(subset-closed_closure_of Y) #);
coherence
 TopStruct(# X,(subset-closed_closure_of Y) #) is strict SimplicialComplexStr of X
proof
 [#] TopStruct(# X,(subset-closed_closure_of Y) #) = X ;
hence  TopStruct(# X,(subset-closed_closure_of Y) #) is strict SimplicialComplexStr of X by Def9; ::_thesis: verum
end;
end;

:: deftheorem  defines Complex_of SIMPLEX0:def_11_:_
 for X being set
for Y being Subset-Family of X holds Complex_of Y = TopStruct(# X,(subset-closed_closure_of Y) #);

registration
let X be set ;
let Y be Subset-Family of X;
cluster Complex_of Y ->  strict subset-closed total ;
coherence
 ( Complex_of Y is total & Complex_of Y is subset-closed )
proof
 ( [#] (Complex_of Y) = X & subset-closed_closure_of Y = the_family_of TopStruct(# X,(subset-closed_closure_of Y) #) ) ;
hence  ( Complex_of Y is total & Complex_of Y is subset-closed ) by Def10, MATROID0:def_3; ::_thesis: verum
end;
end;

registration
let X be set ;
let Y be non empty Subset-Family of X;
cluster Complex_of Y ->  strict with_empty_element ;
coherence
 not Complex_of Y is with_non-empty_elements by Def8;
end;

registration
let X be set ;
let Y be finite-membered Subset-Family of X;
cluster Complex_of Y ->  strict finite-membered ;
coherence
 Complex_of Y is finite-membered
proof
 subset-closed_closure_of Y = the_family_of (Complex_of Y) ;
hence  Complex_of Y is finite-membered by MATROID0:def_6; ::_thesis: verum
end;
end;

registration
let X be set ;
let Y be finite finite-membered Subset-Family of X;
cluster Complex_of Y ->  strict finite-vertices ;
coherence
 Complex_of Y is finite-vertices
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 (Complex_of Y) c= union (bool (union Y)) by ZFMISC_1:77;
 union (bool (union Y)) = union Y by ZFMISC_1:81;
then  Vertices (Complex_of Y) c= union Y by A1, Lm5;
hence  Complex_of Y is finite-vertices by Def5; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:21
for K being SimplicialComplexStr st K is subset-closed holds
TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K
proof
let K be SimplicialComplexStr; ::_thesis: ( K is subset-closed implies TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K )
assume  K is subset-closed ; ::_thesis: TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K
then  the_family_of K is subset-closed ;
hence  TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K by Th7; ::_thesis: verum
end;

definition
let X be set ;
mode SimplicialComplex of X is subset-closed finite-membered 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 Element of bool the carrier of K;
coherence
 for b1 being Subset of K st b1 is empty holds
b1 is simplex-like
proof
let S be Subset of K; ::_thesis: ( S is empty implies S is simplex-like )
assume A1: S is empty ; ::_thesis: S is simplex-like
 the topology of K is with_empty_element by Def8;
then  S in the topology of K by A1, SETFAM_1:def_8;
hence  S is simplex-like by PRE_TOPC:def_2; ::_thesis: verum
end;
cluster empty simplex-like for Element of bool the carrier of K;
existence
 ex b1 being Simplex of K st b1 is empty
proof
 {} K is simplex-like ;
hence  ex b1 being Simplex of K st b1 is empty ; ::_thesis: verum
end;
end;

registration
let K be non void finite-membered SimplicialComplexStr;
cluster finite simplex-like for Element of bool the carrier of K;
existence
 ex b1 being Simplex of K st b1 is finite
proof
consider S being set  such that
A1: S in the topology of K by XBOOLE_0:def_1;
reconsider S = S as Simplex of K by A1, PRE_TOPC:def_2;
 S is finite ;
hence  ex b1 being Simplex of K st b1 is finite ; ::_thesis: verum
end;
end;

begin

definition
let K be SimplicialComplexStr;
func degree K ->  ext-real number  means :Def12: :: SIMPLEX0:def 12
( ( for S being finite Subset of K st S is simplex-like holds
card S <= it + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = it + 1 ) ) if ( not K is void & K is finite-degree )
it = - 1 if K is void
otherwise it = +infty ;
existence
 ( ( not K is void & K is finite-degree implies ex b1 being ext-real number st
( ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) ) ) & ( K is void implies ex b1 being ext-real number st b1 = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b1 being ext-real number st b1 = +infty ) )
proof
now__::_thesis:_(_not_K_is_void_&_K_is_finite-degree_implies_ex_D_being_set_st_
(_(_for_S_being_finite_Subset_of_K_st_S_is_simplex-like_holds_
card_S_<=_D_+_1_)_&_ex_S_being_Subset_of_K_st_
(_S_is_simplex-like_&_not_card_S_<>_D_+_1_)_)_)
defpred S1[ Nat] means  for S being finite Subset of K st S is simplex-like holds
card S <= $1;
assume A1: ( not K is void & K is finite-degree ) ; ::_thesis: ex D being set st
( ( for S being finite Subset of K st S is simplex-like holds
card S <= D + 1 ) & ex S being Subset of K st
( S is simplex-like & not card S <> D + 1 ) )
then A2: the_family_of K is finite-membered by MATROID0:def_6;
A3: ex n being Nat st S1[n] by A1, MATROID0:def_7;
consider k being Nat such that
A4: S1[k] and
A5: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A3);
take D = k - 1; ::_thesis: ( ( for S being finite Subset of K st S is simplex-like holds
card S <= D + 1 ) & ex S being Subset of K st
( S is simplex-like & not card S <> D + 1 ) )
thus  for S being finite Subset of K st S is simplex-like holds
card S <= D + 1 by A4; ::_thesis: ex S being Subset of K st
( S is simplex-like & not card S <> D + 1 )
assume A6: for S being Subset of K st S is simplex-like holds
card S <> D + 1 ; ::_thesis: contradiction
percases ( k = 0 or k > 0 ) ;
supposeA7: k = 0 ; ::_thesis: contradiction
consider S being set  such that
A8: S in the topology of K by A1, XBOOLE_0:def_1;
reconsider S = S as finite Subset of K by A2, A8;
A9: S is simplex-like by A8, PRE_TOPC:def_2;
then  card S = 0 by A4, A7;
hence  contradiction by A6, A7, A9; ::_thesis: verum
end;
suppose k > 0 ; ::_thesis: contradiction
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
 S1[k1]
proof
let S be finite Subset of K; ::_thesis: ( S is simplex-like implies card S <= k1 )
assume A10: S is simplex-like ; ::_thesis: card S <= k1
then  card S <= k1 + 1 by A4;
then  card S < k1 + 1 by A6, A10, XXREAL_0:1;
hence  card S <= k1 by NAT_1:13; ::_thesis: verum
end;
then  k1 + 1 <= k1 by A5;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
hence  ( ( not K is void & K is finite-degree implies ex b1 being ext-real number st
( ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) ) ) & ( K is void implies ex b1 being ext-real number st b1 = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b1 being ext-real number st b1 = +infty ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ext-real number holds
( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= b2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b2 + 1 ) implies b1 = b2 ) & ( K is void & b1 = - 1 & b2 = - 1 implies b1 = b2 ) & ( ( K is void or not K is finite-degree ) & not K is void & b1 = +infty & b2 = +infty implies b1 = b2 ) )
proof
let D1, D2 be ext-real number ; ::_thesis: ( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D2 + 1 ) implies D1 = D2 ) & ( K is void & D1 = - 1 & D2 = - 1 implies D1 = D2 ) & ( ( K is void or not K is finite-degree ) & not K is void & D1 = +infty & D2 = +infty implies D1 = D2 ) )
now__::_thesis:_(_not_K_is_void_&_K_is_finite-degree_&_(_for_S_being_finite_Subset_of_K_st_S_is_simplex-like_holds_
card_S_<=_D1_+_1_)_&_ex_S1_being_Subset_of_K_st_
(_S1_is_simplex-like_&_card_S1_=_D1_+_1_)_&_(_for_S_being_finite_Subset_of_K_st_S_is_simplex-like_holds_
card_S_<=_D2_+_1_)_&_ex_S2_being_Subset_of_K_st_
(_S2_is_simplex-like_&_card_S2_=_D2_+_1_)_implies_D1_=_D2_)
assume A11: ( not K is void & K is finite-degree ) ; ::_thesis: ( ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S1 being Subset of K st
( S1 is simplex-like & card S1 = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
assume A12: for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ; ::_thesis: ( ex S1 being Subset of K st
( S1 is simplex-like & card S1 = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
given S1 being Subset of K such that A13: ( S1 is simplex-like & card S1 = D1 + 1 ) ; ::_thesis: ( ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
assume A14: for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ; ::_thesis: ( ex S2 being Subset of K st
( S2 is simplex-like & card S2 = D2 + 1 ) implies D1 = D2 )
given S2 being Subset of K such that A15: ( S2 is simplex-like & card S2 = D2 + 1 ) ; ::_thesis: D1 = D2
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; ::_thesis: verum
end;
hence  ( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= D1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= D2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = D2 + 1 ) implies D1 = D2 ) & ( K is void & D1 = - 1 & D2 = - 1 implies D1 = D2 ) & ( ( K is void or not K is finite-degree ) & not K is void & D1 = +infty & D2 = +infty implies D1 = D2 ) ) ; ::_thesis: verum
end;
consistency
 for b1 being ext-real number st not K is void & K is finite-degree & K is void holds
( ( ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) ) iff b1 = - 1 ) ;
end;

:: deftheorem Def12 defines degree SIMPLEX0:def_12_:_
 for K being SimplicialComplexStr
for b2 being ext-real number holds
( ( not K is void & K is finite-degree implies ( b2 = degree K iff ( ( for S being finite Subset of K st S is simplex-like holds
card S <= b2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b2 + 1 ) ) ) ) & ( K is void implies ( b2 = degree K iff b2 = - 1 ) ) & ( ( K is void or not K is finite-degree ) & not K is void implies ( b2 = degree K iff b2 = +infty ) ) );

registration
let K be finite-degree SimplicialComplexStr;
cluster(degree K) + 1 ->  natural ;
coherence
 (degree K) + 1 is natural
proof
percases ( K is void or not K is void ) ;
suppose K is void ; ::_thesis: (degree K) + 1 is natural
then (degree K) + 1 = (- 1) + 1 by Def12
.= 0 ;
hence  (degree K) + 1 is natural ; ::_thesis: verum
end;
suppose not K is void ; ::_thesis: (degree K) + 1 is natural
then consider S being 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, PRE_TOPC:def_2;
then  S is finite ;
hence  (degree K) + 1 is natural by A2; ::_thesis: verum
end;
end;
end;
cluster degree K ->  ext-real integer ;
coherence
 degree K is integer
proof
 degree K = ((degree K) + 1) - 1 by XXREAL_3:24;
hence  degree K is integer ; ::_thesis: verum
end;
end;

theorem Th22: :: SIMPLEX0:22
for K being SimplicialComplexStr holds
( degree K = - 1 iff K is empty-membered )
proof
let K be SimplicialComplexStr; ::_thesis: ( degree K = - 1 iff K is empty-membered )
percases ( K is void or not K is void ) ;
suppose K is void ; ::_thesis: ( degree K = - 1 iff K is empty-membered )
hence  ( degree K = - 1 iff K is empty-membered ) by Def12; ::_thesis: verum
end;
supposeA1: not K is void ; ::_thesis: ( degree K = - 1 iff K is empty-membered )
hereby  ::_thesis: ( K is empty-membered implies degree K = - 1 )
assume A2: degree K = - 1 ; ::_thesis: not K is with_non-empty_element
then A3: K is finite-degree by A1, Def12;
assume  K is with_non-empty_element ; ::_thesis: contradiction
then  the topology of K is with_non-empty_element by Def7;
then consider S being non empty set  such that
A4: S in the topology of K by SETFAM_1:def_10;
reconsider S = S as Subset of K by A4;
A5: S is simplex-like by A4, PRE_TOPC:def_2;
then reconsider S = 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 ; ::_thesis: verum
end;
assume A6: K is empty-membered ; ::_thesis: degree K = - 1
then consider S being 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, PRE_TOPC:def_2;
assume  degree K <> - 1 ; ::_thesis: contradiction
then  card S <> (- 1) + 1 by A8, XXREAL_3:11;
then A10: not S is empty ;
 the topology of K is empty-membered by A6, Def7;
hence  contradiction by A9, A10, SETFAM_1:def_10; ::_thesis: verum
end;
end;
end;

theorem Th23: :: SIMPLEX0:23
for K being SimplicialComplexStr holds - 1 <= degree K
proof
let K be SimplicialComplexStr; ::_thesis: - 1 <= degree K
percases ( K is void or ( not K is void & K is finite-degree ) or ( not K is void & not K is finite-degree ) ) ;
suppose K is void ; ::_thesis: - 1 <= degree K
hence  - 1 <= degree K by Def12; ::_thesis: verum
end;
supposeA1: ( not K is void & K is finite-degree ) ; ::_thesis: - 1 <= degree K
then reconsider d = degree K as Integer ;
 ( 0 = (- 1) + 1 & d + 1 >= 0 ) by A1;
hence  - 1 <= degree K by XREAL_1:6; ::_thesis: verum
end;
suppose ( not K is void & not K is finite-degree ) ; ::_thesis: - 1 <= degree K
hence  - 1 <= degree K by Def12; ::_thesis: verum
end;
end;
end;

theorem Th24: :: SIMPLEX0:24
for K being SimplicialComplexStr
for S being finite Subset of K st S is simplex-like holds
card S <= (degree K) + 1
proof
let K be SimplicialComplexStr; ::_thesis: for S being finite Subset of K st S is simplex-like holds
card S <= (degree K) + 1
let S be finite Subset of K; ::_thesis: ( S is simplex-like implies card S <= (degree K) + 1 )
assume A1: S is simplex-like ; ::_thesis: card S <= (degree K) + 1
 S in the topology of K by A1, PRE_TOPC:def_2;
then A2: not K is void by PENCIL_1:def_4;
percases ( K is finite-degree or not K is finite-degree ) ;
suppose K is finite-degree ; ::_thesis: card S <= (degree K) + 1
hence  card S <= (degree K) + 1 by A1, A2, Def12; ::_thesis: verum
end;
suppose not K is finite-degree ; ::_thesis: card S <= (degree K) + 1
then  degree K = +infty by A2, Def12;
then  (degree K) + 1 = +infty by XXREAL_3:def_2;
hence  card S <= (degree K) + 1 by XXREAL_0:3; ::_thesis: verum
end;
end;
end;

theorem Th25: :: SIMPLEX0:25
for i being Integer
for K being SimplicialComplexStr st ( not K is void or i >= - 1 ) holds
( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )
proof
let i be Integer; ::_thesis: for K being SimplicialComplexStr st ( not K is void or i >= - 1 ) holds
( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )
let K be SimplicialComplexStr; ::_thesis: ( ( not K is void or i >= - 1 ) implies ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) ) )
assume A1: ( not K is void or i >= - 1 ) ; ::_thesis: ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )
percases ( K is void or not K is void ) ;
supposeA2: K is void ; ::_thesis: ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )
A3: now__::_thesis:_for_S_being_finite_Subset_of_K_st_S_is_simplex-like_holds_
card_S_<=_i_+_1
let S be finite Subset of K; ::_thesis: ( S is simplex-like implies card S <= i + 1 )
assume  S is simplex-like ; ::_thesis: card S <= i + 1
then  S in the topology of K by PRE_TOPC:def_2;
hence  card S <= i + 1 by A2, PENCIL_1:def_4; ::_thesis: verum
end;
 K is empty-membered by A2;
hence  ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) ) by A1, A2, A3, Th22; ::_thesis: verum
end;
supposeA4: not K is void ; ::_thesis: ( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )
hereby  ::_thesis: ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) implies degree K <= i )
assume A5: degree K <= i ; ::_thesis: ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) )
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 ; ::_thesis: for S being finite Subset of K st S is simplex-like holds
card S <= i + 1
let S be finite Subset of K; ::_thesis: ( S is simplex-like implies card S <= i + 1 )
assume A8: S is simplex-like ; ::_thesis: card S <= i + 1
 ( ( not K is void & K is 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; ::_thesis: verum
end;
assume that
A9: K is finite-membered and
A10: for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ; ::_thesis: degree K <= i
consider S being set  such that
A11: S in the topology of K by A4, XBOOLE_0:def_1;
reconsider S = S as Subset of K by A11;
A12: S is simplex-like by A11, PRE_TOPC:def_2;
then reconsider S = S as finite Subset of K by A4, A9;
 card S <= i + 1 by A10, A12;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;
 for A being finite Subset of K st A is open holds
card A <= i1 by A10;
then A13: K is finite-degree by A9, MATROID0:def_7;
then reconsider d = degree K as Integer ;
 ex S1 being Subset of K st
( S1 is simplex-like & card S1 = (degree K) + 1 ) by A4, A13, Def12;
then  d + 1 <= i + 1 by A4, A9, A10;
hence  degree K <= i by XREAL_1:6; ::_thesis: verum
end;
end;
end;

theorem :: SIMPLEX0:26
for X being set
for A being finite Subset of X holds degree (Complex_of {A}) = (card A) - 1
proof
let X be set ; ::_thesis: for A being finite Subset of X holds degree (Complex_of {A}) = (card A) - 1
let A be finite Subset of X; ::_thesis: degree (Complex_of {A}) = (card A) - 1
set C = Complex_of {A};
A1: the topology of (Complex_of {A}) = bool A by Th4;
now__::_thesis:_for_S_being_finite_Subset_of_(Complex_of_{A})_st_S_is_simplex-like_holds_
card_S_<=_((card_A)_-_1)_+_1
let S be finite Subset of (Complex_of {A}); ::_thesis: ( S is simplex-like implies card S <= ((card A) - 1) + 1 )
assume  S is simplex-like ; ::_thesis: card S <= ((card A) - 1) + 1
then  S in the topology of (Complex_of {A}) by PRE_TOPC:def_2;
hence  card S <= ((card A) - 1) + 1 by A1, NAT_1:43; ::_thesis: verum
end;
then A2: degree (Complex_of {A}) <= (card A) - 1 by Th25;
 A c= A ;
then reconsider A1 = A as finite Simplex of (Complex_of {A}) by A1, PRE_TOPC:def_2;
 ( card A = ((card A) - 1) + 1 & card A1 <= (degree (Complex_of {A})) + 1 ) by Def12;
then  (card A) - 1 <= degree (Complex_of {A}) by XREAL_1:8;
hence  (card A) - 1 = degree (Complex_of {A}) by A2, XXREAL_0:1; ::_thesis: verum
end;

begin

definition
let X be set ;
let KX be SimplicialComplexStr of X;
mode SubSimplicialComplex of KX ->  SimplicialComplex of X means :Def13: :: SIMPLEX0:def 13
( [#] it c= [#] KX & the topology of it c= the topology of KX );
existence
 ex b1 being SimplicialComplex of X st
( [#] b1 c= [#] KX & the topology of b1 c= the topology of KX )
proof
set T = TopStruct(# 0,({} (bool 0)) #);
 ( the_family_of TopStruct(# 0,({} (bool 0)) #) is empty & [#] TopStruct(# 0,({} (bool 0)) #) c= X ) by XBOOLE_1:2;
then reconsider T = TopStruct(# 0,({} (bool 0)) #) as SimplicialComplex of X by Def9, MATROID0:def_3, MATROID0:def_6;
take  T ; ::_thesis: ( [#] T c= [#] KX & the topology of T c= the topology of KX )
thus  ( [#] T c= [#] KX & the topology of T c= the topology of KX ) by XBOOLE_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines SubSimplicialComplex SIMPLEX0:def_13_:_
 for X being set
for KX being SimplicialComplexStr of X
for b3 being SimplicialComplex of X holds
( b3 is SubSimplicialComplex of KX iff ( [#] b3 c= [#] KX & the topology of b3 c= the topology of KX ) );


registration
let X be set ;
let KX be SimplicialComplexStr of X;
cluster empty strict void subset-closed finite-membered for SubSimplicialComplex of KX;
existence
 ex b1 being SubSimplicialComplex of KX st
( b1 is empty & b1 is void & b1 is strict )
proof
set C = Complex_of ({} (bool {}));
 the topology of (Complex_of ({} (bool {}))) = {} ;
then A1: ( [#] (Complex_of ({} (bool {}))) c= [#] KX & the topology of (Complex_of ({} (bool {}))) c= the topology of KX ) by XBOOLE_1:2;
 [#] (Complex_of ({} (bool {}))) c= X by XBOOLE_1:2;
then  Complex_of ({} (bool {})) is SimplicialComplexStr of X by Def9;
then reconsider C = Complex_of ({} (bool {})) as SubSimplicialComplex of KX by A1, Def13;
take  C ; ::_thesis: ( C is empty & C is void & C is strict )
thus  ( C is empty & C is void & C is strict ) ; ::_thesis: verum
end;
end;

registration
let X be set ;
let KX be void SimplicialComplexStr of X;
cluster  ->  void for SubSimplicialComplex of KX;
coherence
 for b1 being SubSimplicialComplex of KX holds b1 is void
proof
let S be SubSimplicialComplex of KX; ::_thesis: S is void
 ( the topology of S c= the topology of KX & the topology of KX is empty ) by Def13, PENCIL_1:def_4;
hence  S is void ; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
let KD be non void subset-closed SimplicialComplexStr of D;
cluster non void subset-closed finite-membered for SubSimplicialComplex of KD;
existence
 not for b1 being SubSimplicialComplex of KD holds b1 is void
proof
A1: the_family_of KD is subset-closed ;
consider x being set  such that
A2: x in the topology of KD by XBOOLE_0:def_1;
percases ( x is empty or not x is empty ) ;
suppose x is empty ; ::_thesis: not for b1 being SubSimplicialComplex of KD holds b1 is void
then reconsider x = x as empty Subset of KD by A2;
set S = Complex_of {x};
A3: [#] (Complex_of {x}) = [#] KD ;
 [#] KD c= D by Def9;
then reconsider S = Complex_of {x} as SimplicialComplex of D by A3, Def9;
take  S ; ::_thesis: ( S is SubSimplicialComplex of KD & not S is void )
 {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  ( S is SubSimplicialComplex of KD & not S is void ) by A3, Def13; ::_thesis: verum
end;
supposeA4: not x is empty ; ::_thesis: not for b1 being SubSimplicialComplex of KD holds b1 is void
set d = the Element of x;
 the Element of x in x by A4;
then reconsider dd = { the Element of x} as Subset of KD by A2, ZFMISC_1:31;
set S = Complex_of {dd};
A5: [#] (Complex_of {dd}) = [#] KD ;
 [#] KD c= D by Def9;
then reconsider S = Complex_of {dd} as SimplicialComplex of D by A5, Def9;
take  S ; ::_thesis: ( S is SubSimplicialComplex of KD & not S is void )
 dd c= x by A4, ZFMISC_1:31;
then  dd in the topology of KD by A1, A2, CLASSES1:def_1;
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  ( S is SubSimplicialComplex of KD & not S is void ) by A5, Def13; ::_thesis: verum
end;
end;
end;
end;

registration
let X be set ;
let KX be finite-vertices SimplicialComplexStr of X;
cluster  ->  finite-vertices for SubSimplicialComplex of KX;
coherence
 for b1 being SubSimplicialComplex of KX holds b1 is finite-vertices
proof
let SX be SubSimplicialComplex of KX; ::_thesis: SX is finite-vertices
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  SX is finite-vertices by A2, A1, Def5; ::_thesis: verum
end;
end;

registration
let X be set ;
let KX be finite-degree SimplicialComplexStr of X;
cluster  ->  finite-degree for SubSimplicialComplex of KX;
coherence
 for b1 being SubSimplicialComplex of KX holds b1 is finite-degree
proof
let S be SubSimplicialComplex of KX; ::_thesis: S is finite-degree
consider n being Nat such that
A1: for A being finite Subset of KX st A is simplex-like holds
card A <= n by MATROID0:def_7;
thus  S is finite-membered ; :: according to MATROID0:def_7 ::_thesis: ex b1 being set st
for b2 being Element of bool the carrier of S holds
( not b2 is simplex-like or card b2 <= b1 )
take  n ; ::_thesis: for b1 being Element of bool the carrier of S holds
( not b1 is simplex-like or card b1 <= n )
let A be finite Subset of S; ::_thesis: ( not A is simplex-like or card A <= n )
assume  A is simplex-like ; ::_thesis: card A <= n
then A2: A in the topology of S by PRE_TOPC:def_2;
 [#] 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, PRE_TOPC:def_2;
hence  card A <= n by A1; ::_thesis: verum
end;
end;

theorem Th27: :: SIMPLEX0:27
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
let SX be SubSimplicialComplex of KX; ::_thesis: for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
let S1 be SubSimplicialComplex of SX; ::_thesis: S1 is SubSimplicialComplex of KX
 ( [#] SX c= [#] KX & [#] S1 c= [#] SX ) by Def13;
then A1: [#] S1 c= [#] KX by XBOOLE_1:1;
 ( 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 by XBOOLE_1:1;
hence  S1 is SubSimplicialComplex of KX by A1, Def13; ::_thesis: verum
end;

theorem Th28: :: SIMPLEX0:28
for X being set
for KX being SimplicialComplexStr of X
for A being Subset of KX
for S being 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 X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for A being Subset of KX
for S being 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
let KX be SimplicialComplexStr of X; ::_thesis: for A being Subset of KX
for S being 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
let A be Subset of KX; ::_thesis: for S being 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
let S be finite-membered Subset-Family of A; ::_thesis: ( subset-closed_closure_of S c= the topology of KX implies Complex_of S is strict SubSimplicialComplex of KX )
assume A1: subset-closed_closure_of S c= the topology of KX ; ::_thesis: Complex_of S is strict SubSimplicialComplex of KX
set C = Complex_of S;
 [#] KX c= X by Def9;
then  [#] (Complex_of S) c= X by XBOOLE_1:1;
then  ( [#] (Complex_of S) c= [#] KX & Complex_of S is strict SimplicialComplexStr of X ) by Def9;
hence  Complex_of S is strict SubSimplicialComplex of KX by A1, Def13; ::_thesis: verum
end;

theorem :: SIMPLEX0:29
for X being set
for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX
for S being finite-membered Subset-Family of A st S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
proof
let X be set ; ::_thesis: for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX
for S being finite-membered Subset-Family of A st S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let KX be subset-closed SimplicialComplexStr of X; ::_thesis: for A being Subset of KX
for S being finite-membered Subset-Family of A st S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let A be Subset of KX; ::_thesis: for S being finite-membered Subset-Family of A st S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let S be finite-membered Subset-Family of A; ::_thesis: ( S c= the topology of KX implies Complex_of S is strict SubSimplicialComplex of KX )
A1: the_family_of KX is subset-closed ;
assume  S c= the topology of KX ; ::_thesis: Complex_of S is strict SubSimplicialComplex of KX
hence  Complex_of S is strict SubSimplicialComplex of KX by A1, Th3, Th28; ::_thesis: verum
end;

theorem :: SIMPLEX0:30
for X being set
for Y1, Y2 being 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 X be set ; ::_thesis: for Y1, Y2 being Subset-Family of X st Y1 is finite-membered & Y1 is_finer_than Y2 holds
Complex_of Y1 is SubSimplicialComplex of Complex_of Y2
let Y1, Y2 be Subset-Family of X; ::_thesis: ( Y1 is finite-membered & Y1 is_finer_than Y2 implies Complex_of Y1 is SubSimplicialComplex of Complex_of Y2 )
assume that
A1: Y1 is finite-membered and
A2: Y1 is_finer_than Y2 ; ::_thesis: Complex_of Y1 is SubSimplicialComplex of Complex_of Y2
set C1 = Complex_of Y1;
set C2 = Complex_of Y2;
A3: ( [#] (Complex_of Y1) = X & [#] (Complex_of Y2) = X ) ;
 subset-closed_closure_of Y1 c= subset-closed_closure_of Y2 by A2, Th6;
hence  Complex_of Y1 is SubSimplicialComplex of Complex_of Y2 by A1, A3, Def13; ::_thesis: verum
end;

theorem :: SIMPLEX0:31
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX
let SX be SubSimplicialComplex of KX; ::_thesis: Vertices SX c= Vertices KX
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Vertices SX or x in Vertices KX )
assume A1: x in Vertices SX ; ::_thesis: x in Vertices KX
then reconsider v = x as Element of SX ;
 v is vertex-like by A1, Def4;
then consider S being Subset of SX such that
A2: S is simplex-like and
A3: v in S by Def3;
A4: the topology of SX c= the topology of KX by Def13;
A5: S in the topology of SX by A2, PRE_TOPC:def_2;
then  S in the topology of KX by A4;
then reconsider S = S as Subset of KX ;
 v in S by A3;
then reconsider v = v as Element of KX ;
 S is simplex-like by A4, A5, PRE_TOPC:def_2;
then  v is vertex-like by A3, Def3;
hence  x in Vertices KX by Def4; ::_thesis: verum
end;

theorem Th32: :: SIMPLEX0:32
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds degree SX <= degree KX
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds degree SX <= degree KX
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX holds degree SX <= degree KX
let SX be SubSimplicialComplex of KX; ::_thesis: degree SX <= degree KX
percases ( not SX is finite-degree or SX is void or ( not SX is void & SX is finite-degree ) ) ;
supposeA1: not SX is finite-degree ; ::_thesis: degree SX <= degree KX
 not SX is void
proof
assume  SX is void ; ::_thesis: contradiction
then  SX is empty-membered ;
hence  contradiction by A1; ::_thesis: verum
end;
then  ( not KX is finite-degree & not KX is void & degree SX = +infty ) by A1, Def12;
hence  degree SX <= degree KX by Def12; ::_thesis: verum
end;
suppose SX is void ; ::_thesis: degree SX <= degree KX
then  degree SX = - 1 by Def12;
hence  degree SX <= degree KX by Th23; ::_thesis: verum
end;
supposeA2: ( not SX is void & SX is finite-degree ) ; ::_thesis: degree SX <= degree KX
then A3: not KX is void ;
percases ( not KX is finite-degree or KX is finite-degree ) ;
suppose not KX is finite-degree ; ::_thesis: degree SX <= degree KX
then  degree KX = +infty by A3, Def12;
hence  degree SX <= degree KX by XXREAL_0:3; ::_thesis: verum
end;
supposeA4: KX is finite-degree ; ::_thesis: degree SX <= degree KX
A5: the topology of SX c= the topology of KX by Def13;
consider S being 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, PRE_TOPC:def_2;
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, PRE_TOPC:def_2;
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  degree SX <= degree KX by A9, XXREAL_3:24; ::_thesis: verum
end;
end;
end;
end;
end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let SX be SubSimplicialComplex of KX;
attrSX is maximal  means :Def14: :: SIMPLEX0:def 14
 for A being Subset of SX st A in the topology of KX holds
A is simplex-like ;
end;

:: deftheorem Def14 defines maximal SIMPLEX0:def_14_:_
 for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds
( SX is maximal iff for A being Subset of SX st A in the topology of KX holds
A is simplex-like );

theorem Th33: :: SIMPLEX0:33
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds
( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds
( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX holds
( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
let SX be SubSimplicialComplex of KX; ::_thesis: ( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
hereby  ::_thesis: ( (bool ([#] SX)) /\ the topology of KX c= the topology of SX implies SX is maximal )
assume A1: SX is maximal ; ::_thesis: (bool ([#] SX)) /\ the topology of KX c= the topology of SX
thus  (bool ([#] SX)) /\ the topology of KX c= the topology of SX ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (bool ([#] SX)) /\ the topology of KX or x in the topology of SX )
assume A2: x in (bool ([#] SX)) /\ the topology of KX ; ::_thesis: x in the topology of SX
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, Def14;
hence  x in the topology of SX by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
assume A3: (bool ([#] SX)) /\ the topology of KX c= the topology of SX ; ::_thesis: SX is maximal
let A be Subset of SX; :: according to SIMPLEX0:def_14 ::_thesis: ( A in the topology of KX implies A is simplex-like )
assume  A in the topology of KX ; ::_thesis: A is simplex-like
then  A in (bool ([#] SX)) /\ the topology of KX by XBOOLE_0:def_4;
hence  A is simplex-like by A3, PRE_TOPC:def_2; ::_thesis: verum
end;

registration
let X be set ;
let KX be SimplicialComplexStr of X;
cluster strict subset-closed finite-membered maximal for SubSimplicialComplex of KX;
existence
 ex b1 being SubSimplicialComplex of KX st
( b1 is maximal & b1 is strict )
proof
set B = (bool {}) /\ the topology of KX;
reconsider B = (bool {}) /\ the topology of KX 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 ; ::_thesis: ( C is maximal & C is strict )
 ( C = TopStruct(# ({} KX),B #) & bool ([#] C) = bool {} ) by Th7;
hence  ( C is maximal & C is strict ) by Th33; ::_thesis: verum
end;
end;

theorem Th34: :: SIMPLEX0:34
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
let SX be SubSimplicialComplex of KX; ::_thesis: for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
let S1 be SubSimplicialComplex of SX; ::_thesis: ( SX is maximal & S1 is maximal implies S1 is maximal SubSimplicialComplex of KX )
reconsider s1 = S1 as SubSimplicialComplex of KX by Th27;
assume that
A1: SX is maximal and
A2: S1 is maximal ; ::_thesis: S1 is maximal SubSimplicialComplex of KX
A3: [#] S1 c= [#] SX by Def13;
now__::_thesis:_for_A_being_Subset_of_s1_st_A_in_the_topology_of_KX_holds_
A_is_simplex-like
let A be Subset of s1; ::_thesis: ( A in the topology of KX implies A is simplex-like )
reconsider a = A as Subset of SX by A3, XBOOLE_1:1;
assume  A in the topology of KX ; ::_thesis: A is simplex-like
then  a is simplex-like by A1, Def14;
then  a in the topology of SX by PRE_TOPC:def_2;
hence  A is simplex-like by A2, Def14; ::_thesis: verum
end;
hence  S1 is maximal SubSimplicialComplex of KX by Def14; ::_thesis: verum
end;

theorem :: SIMPLEX0:35
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
let SX be SubSimplicialComplex of KX; ::_thesis: for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
let S1 be SubSimplicialComplex of SX; ::_thesis: ( S1 is maximal SubSimplicialComplex of KX implies S1 is maximal )
assume  S1 is maximal SubSimplicialComplex of KX ; ::_thesis: S1 is maximal
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, XBOOLE_1:1;
hence  S1 is maximal by Th33; ::_thesis: verum
end;

theorem Th36: :: SIMPLEX0:36
for X being set
for KX being SimplicialComplexStr of X
for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
let KX be SimplicialComplexStr of X; ::_thesis: for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
let K1, K2 be maximal SubSimplicialComplex of KX; ::_thesis: ( [#] K1 = [#] K2 implies TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) )
assume A1: [#] K1 = [#] K2 ; ::_thesis: TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
set TOP1 = the topology of K1;
set TOP2 = the topology of K2;
set TOP = the topology of KX;
A2: the topology of KX /\ (bool ([#] K2)) c= the topology of K2 by Th33;
 the topology of K1 c= the topology of KX by Def13;
then A3: the topology of K1 c= the topology of KX /\ (bool ([#] K1)) by XBOOLE_1:19;
 the topology of K2 c= the topology of KX by Def13;
then A4: the topology of K2 c= the topology of KX /\ (bool ([#] K2)) by XBOOLE_1:19;
 the topology of KX /\ (bool ([#] K1)) c= the topology of K1 by Th33;
then  the topology of K1 = the topology of KX /\ (bool ([#] K1)) by A3, XBOOLE_0:def_10
.= the topology of K2 by A1, A2, A4, XBOOLE_0:def_10 ;
hence  TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) by A1; ::_thesis: verum
end;

definition
let X be set ;
let KX be subset-closed SimplicialComplexStr of X;
let A be Subset of KX;
assume A1: (bool A) /\ the topology of KX is finite-membered ;
funcKX | A ->  strict maximal SubSimplicialComplex of KX means :Def15: :: SIMPLEX0:def 15
 [#] it = A;
existence
 ex b1 being strict maximal SubSimplicialComplex of KX st [#] b1 = A
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 #);
A1: ( [#] TopStruct(# A,BA #) c= [#] KX & the topology of TopStruct(# A,BA #) c= the topology of KX ) by XBOOLE_1:17;
 BA = the_family_of TopStruct(# A,BA #) ;
then A2: ( TopStruct(# A,BA #) is subset-closed & TopStruct(# A,BA #) is finite-membered ) by MATROID0:def_3, MATROID0:def_6;
 [#] KX c= X by Def9;
then  [#] TopStruct(# A,BA #) c= X by XBOOLE_1:1;
then  TopStruct(# A,BA #) is SimplicialComplexStr of X by Def9;
then reconsider KA = TopStruct(# A,BA #) as strict maximal SubSimplicialComplex of KX by A1, A2, Def13, Th33;
take  KA ; ::_thesis: [#] KA = A
thus  [#] KA = A ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict maximal SubSimplicialComplex of KX st [#] b1 = A & [#] b2 = A holds
b1 = b2 by Th36;
end;

:: deftheorem Def15 defines | SIMPLEX0:def_15_:_
 for X being set
for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX st (bool A) /\ the topology of KX is finite-membered holds
for b4 being strict maximal SubSimplicialComplex of KX holds
( b4 = KX | A iff [#] b4 = A );

definition
let X be set ;
let SC be SimplicialComplex of X;
let A be Subset of SC;
redefine func SC | A means :Def16: :: SIMPLEX0:def 16
 [#] it = A;
compatibility
 for b1 being strict maximal SubSimplicialComplex of SC holds
( b1 = SC | A iff [#] b1 = A )
proof
let KA be strict maximal SubSimplicialComplex of SC; ::_thesis: ( KA = SC | A iff [#] KA = A )
 ( 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  ( KA = SC | A iff [#] KA = A ) by Def15; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines | SIMPLEX0:def_16_:_
 for X being set
for SC being SimplicialComplex of X
for A being Subset of SC
for b4 being strict maximal SubSimplicialComplex of SC holds
( b4 = SC | A iff [#] b4 = A );

theorem Th37: :: SIMPLEX0:37
for X being set
for SC being SimplicialComplex of X
for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC
proof
let X be set ; ::_thesis: for SC being SimplicialComplex of X
for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC
let SC be SimplicialComplex of X; ::_thesis: for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC
let A be Subset of SC; ::_thesis: the topology of (SC | A) = (bool A) /\ the topology 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  the topology of (SC | A) = (bool A) /\ the topology of SC by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SIMPLEX0:38
for X being set
for SC being SimplicialComplex of X
for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
proof
let X be set ; ::_thesis: for SC being SimplicialComplex of X
for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
let SC be SimplicialComplex of X; ::_thesis: for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
let A, B be Subset of SC; ::_thesis: for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
let B1 be Subset of (SC | A); ::_thesis: ( B1 = B implies (SC | A) | B1 = SC | B )
reconsider SCAB = (SC | A) | B1 as strict maximal SubSimplicialComplex of SC by Th34;
assume A1: B1 = B ; ::_thesis: (SC | A) | B1 = SC | B
 [#] SCAB = B1 by Def16;
hence  (SC | A) | B1 = SC | B by A1, Def16; ::_thesis: verum
end;

theorem :: SIMPLEX0:39
for X being set
for SC being SimplicialComplex of X holds SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #)
proof
let X be set ; ::_thesis: for SC being SimplicialComplex of X holds SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #)
let SC be SimplicialComplex of X; ::_thesis: SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #)
set T = TopStruct(# the carrier of SC, the topology of SC #);
A1: ( [#] TopStruct(# the carrier of SC, the topology of SC #) c= [#] SC & (bool ([#] TopStruct(# the carrier of SC, the topology of SC #))) /\ the topology of SC = the topology of SC ) by XBOOLE_1:28;
 ( the_family_of SC = the_family_of TopStruct(# the carrier of SC, the topology of SC #) & the_family_of SC is finite-membered & the_family_of SC is subset-closed ) by MATROID0:def_6;
then A2: ( TopStruct(# the carrier of SC, the topology of SC #) is finite-membered & TopStruct(# the carrier of SC, the topology of SC #) is subset-closed ) by MATROID0:def_3, MATROID0:def_6;
 [#] SC c= X by Def9;
then  [#] TopStruct(# the carrier of SC, the topology of SC #) c= X ;
then  TopStruct(# the carrier of SC, the topology of SC #) is SimplicialComplexStr of X by Def9;
then reconsider T = TopStruct(# the carrier of SC, the topology of SC #) as maximal SubSimplicialComplex of SC by A1, A2, Def13, Th33;
 [#] T = [#] SC ;
hence  SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #) by Def16; ::_thesis: verum
end;

theorem :: SIMPLEX0:40
for X being set
for SC being SimplicialComplex of X
for A, B being Subset of SC st A c= B holds
SC | A is SubSimplicialComplex of SC | B
proof
let X be set ; ::_thesis: for SC being SimplicialComplex of X
for A, B being Subset of SC st A c= B holds
SC | A is SubSimplicialComplex of SC | B
let SC be SimplicialComplex of X; ::_thesis: for A, B being Subset of SC st A c= B holds
SC | A is SubSimplicialComplex of SC | B
let A, B be Subset of SC; ::_thesis: ( A c= B implies SC | A is SubSimplicialComplex of SC | B )
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 ; ::_thesis: SC | A is SubSimplicialComplex of SC | 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  SC | A is SubSimplicialComplex of SC | B by A2, A3, A1, Def13; ::_thesis: verum
end;

registration
cluster integer  ->  finite for set ;
coherence
 for b1 being Integer holds b1 is finite
proof
let i be Integer; ::_thesis: i is finite
 i in (NAT \/ [:{0},NAT:]) \ {[0,0]} by INT_1:def_2, NUMBERS:def_4;
then  ( i in NAT or i in [:{0},NAT:] ) by XBOOLE_0:def_3;
then  ( i in NAT or ex x, y being set st
( x in {0} & y in NAT & i = [x,y] ) ) by ZFMISC_1:def_2;
hence  i is finite ; ::_thesis: verum
end;
end;

begin

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let i be real number ;
func Skeleton_of (KX,i) ->  SimplicialComplexStr of X equals :: SIMPLEX0:def 17
 Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));
coherence
 Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) is SimplicialComplexStr of X
proof
set C = Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));
 [#] KX c= X by Def9;
then  [#] (Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX))) c= X ;
hence  Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) is SimplicialComplexStr of X by Def9; ::_thesis: verum
end;
end;

:: deftheorem  defines Skeleton_of SIMPLEX0:def_17_:_
 for X being set
for KX being SimplicialComplexStr of X
for i being real number holds Skeleton_of (KX,i) = Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));

registration
let X be set ;
let KX be SimplicialComplexStr of X;
cluster Skeleton_of (KX,(- 1)) ->  empty-membered ;
coherence
 Skeleton_of (KX,(- 1)) is empty-membered
proof
assume  Skeleton_of (KX,(- 1)) is with_non-empty_element ; ::_thesis: contradiction
then  the topology of (Skeleton_of (KX,(- 1))) is with_non-empty_element by Def7;
then consider x being non empty set  such that
A1: x in the topology of (Skeleton_of (KX,(- 1))) by SETFAM_1:def_10;
consider b being set  such that
A2: x c= b and
A3: b in the_subsets_with_limited_card (((- 1) + 1), the topology of KX) by A1, Th2;
 card b c= card ((- 1) + 1) by A3, Def2;
then  card b c= {} ;
then  b is empty ;
hence  contradiction by A2; ::_thesis: verum
end;
let i be Integer;
cluster Skeleton_of (KX,i) ->  finite-degree ;
coherence
 Skeleton_of (KX,i) is finite-degree
proof
reconsider i1 = i + 1 as Integer ;
set SUB = the_subsets_with_limited_card ((i + 1), the topology of KX);
set C = Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));
now__::_thesis:_for_A_being_finite_Subset_of_(Complex_of_(the_subsets_with_limited_card_((i_+_1),_the_topology_of_KX)))_st_A_is_open_holds_
card_A_<=_card_i1
let A be finite Subset of (Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX))); ::_thesis: ( A is open implies card A <= card i1 )
assume  A is open ; ::_thesis: card A <= card i1
then  A in subset-closed_closure_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) by PRE_TOPC:def_2;
then consider B being set  such that
A4: ( A c= B & B in the_subsets_with_limited_card ((i + 1), the topology of KX) ) by Th2;
 ( card A c= card B & card B c= card i1 ) by A4, Def2, CARD_1:11;
then  card A c= card i1 by XBOOLE_1:1;
hence  card A <= card i1 by NAT_1:39; ::_thesis: verum
end;
hence  Skeleton_of (KX,i) is finite-degree by MATROID0:def_7; ::_thesis: verum
end;
end;

registration
let X be set ;
let KX be empty-membered SimplicialComplexStr of X;
let i be Integer;
cluster Skeleton_of (KX,i) ->  empty-membered ;
coherence
 Skeleton_of (KX,i) is empty-membered
proof
assume  Skeleton_of (KX,i) is with_non-empty_element ; ::_thesis: contradiction
then  the topology of (Skeleton_of (KX,i)) is with_non-empty_element by Def7;
then consider x being non empty set  such that
A1: x in the topology of (Skeleton_of (KX,i)) by SETFAM_1:def_10;
A2: the topology of KX is empty-membered by Def7;
consider y being set  such that
A3: x c= y and
A4: y in the_subsets_with_limited_card ((i + 1), the topology of KX) by A1, Th2;
 y in the topology of KX by A4, Def2;
then  y is empty by A2, SETFAM_1:def_10;
hence  contradiction by A3; ::_thesis: verum
end;
end;

registration
let D be non empty set ;
let KD be non void subset-closed SimplicialComplexStr of D;
let i be Integer;
cluster Skeleton_of (KD,i) ->  non void ;
coherence
 not Skeleton_of (KD,i) is void
proof
reconsider E = {} as Subset of KD by XBOOLE_1:2;
 ( E in the topology of KD & card E c= card (i + 1) ) by PRE_TOPC:def_2;
then  E in the_subsets_with_limited_card ((i + 1), the topology of KD) by Def2;
hence  not Skeleton_of (KD,i) is void ; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:41
for X being set
for i1, i2 being Integer
for KX being SimplicialComplexStr of X st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
proof
let X be set ; ::_thesis: for i1, i2 being Integer
for KX being SimplicialComplexStr of X st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
let i1, i2 be Integer; ::_thesis: for KX being SimplicialComplexStr of X st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
let KX be SimplicialComplexStr of X; ::_thesis: ( - 1 <= i1 & i1 <= i2 implies Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) )
assume that
A1: - 1 <= i1 and
A2: i1 <= i2 ; ::_thesis: Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
 - 1 <= i2 by A1, A2, XXREAL_0:2;
then A3: (- 1) + 1 <= i2 + 1 by XREAL_1:6;
 (- 1) + 1 <= i1 + 1 by A1, XREAL_1:6;
then reconsider I1 = i1 + 1, I2 = i2 + 1 as Element of NAT by A3, INT_1:3;
 the_subsets_with_limited_card ((i1 + 1), the topology of KX) c= the_subsets_with_limited_card ((i2 + 1), the topology of KX)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_subsets_with_limited_card ((i1 + 1), the topology of KX) or x in the_subsets_with_limited_card ((i2 + 1), the topology of KX) )
 I1 <= I2 by A2, XREAL_1:6;
then A4: card I1 c= card I2 by NAT_1:40;
assume A5: x in the_subsets_with_limited_card ((i1 + 1), the topology of KX) ; ::_thesis: x in the_subsets_with_limited_card ((i2 + 1), the topology of KX)
then  card x c= card I1 by Def2;
then A6: card x c= card I2 by A4, XBOOLE_1:1;
 x in the topology of KX by A5, Def2;
hence  x in the_subsets_with_limited_card ((i2 + 1), the topology of KX) by A6, Def2; ::_thesis: verum
end;
then  the_subsets_with_limited_card ((i1 + 1), the topology of KX) is_finer_than the_subsets_with_limited_card ((i2 + 1), the topology of KX) by SETFAM_1:12;
then A7: 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  Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) by A7, Def13; ::_thesis: verum
end;

definition
let X be set ;
let KX be subset-closed SimplicialComplexStr of X;
let i be Integer;
:: original: Skeleton_of
redefine func Skeleton_of (KX,i) ->  SubSimplicialComplex of KX;
coherence
 Skeleton_of (KX,i) is SubSimplicialComplex of KX
proof
A1: the_subsets_with_limited_card ((i + 1), the topology of KX) c= the topology of KX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_subsets_with_limited_card ((i + 1), the topology of KX) or x in the topology of KX )
assume  x in the_subsets_with_limited_card ((i + 1), the topology of KX) ; ::_thesis: x in the topology of KX
hence  x in the topology of KX by Def2; ::_thesis: verum
end;
 the_family_of KX is subset-closed ;
then  ( [#] (Skeleton_of (KX,i)) = [#] KX & subset-closed_closure_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) c= the topology of KX ) by A1, Th3;
hence  Skeleton_of (KX,i) is SubSimplicialComplex of KX by Def13; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:42
for X being set
for i being Integer
for KX being SimplicialComplexStr of X st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
proof
let X be set ; ::_thesis: for i being Integer
for KX being SimplicialComplexStr of X st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
let i be Integer; ::_thesis: for KX being SimplicialComplexStr of X st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
let KX be SimplicialComplexStr of X; ::_thesis: ( KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered implies i = - 1 )
assume  KX is subset-closed ; ::_thesis: ( not Skeleton_of (KX,i) is empty-membered or KX is empty-membered or i = - 1 )
then A1: the_family_of KX is subset-closed ;
assume A2: Skeleton_of (KX,i) is empty-membered ; ::_thesis: ( KX is empty-membered or i = - 1 )
assume  KX is with_non-empty_element ; ::_thesis: i = - 1
then  the topology of KX is with_non-empty_element by Def7;
then consider x being non empty set  such that
A3: x in the topology of KX by SETFAM_1:def_10;
consider y being set  such that
A4: y in x by XBOOLE_0:def_1;
assume  i <> - 1 ; ::_thesis: contradiction
then  ( {} c= card (i + 1) & not i + 1 is empty ) ;
then  {} in card (i + 1) by CARD_1:3;
then  1 c= card (i + 1) by CARD_2:68;
then A5: card {y} c= card (i + 1) by CARD_1:30;
 {y} c= x by A4, ZFMISC_1:31;
then  {y} in the topology of KX by A1, A3, CLASSES1:def_1;
then  {y} in the_subsets_with_limited_card ((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, Def7;
hence  contradiction by A6, SETFAM_1:def_10; ::_thesis: verum
end;

theorem :: SIMPLEX0:43
for X being set
for i being Integer
for KX being SimplicialComplexStr of X holds degree (Skeleton_of (KX,i)) <= degree KX
proof
let X be set ; ::_thesis: for i being Integer
for KX being SimplicialComplexStr of X holds degree (Skeleton_of (KX,i)) <= degree KX
let i be Integer; ::_thesis: for KX being SimplicialComplexStr of X holds degree (Skeleton_of (KX,i)) <= degree KX
let KX be SimplicialComplexStr of X; ::_thesis: degree (Skeleton_of (KX,i)) <= degree KX
set S = Skeleton_of (KX,i);
percases ( KX is void or Skeleton_of (KX,i) is void or ( not KX is void & KX is finite-degree & not Skeleton_of (KX,i) is void ) or not KX is finite-degree ) ;
suppose ( KX is void or Skeleton_of (KX,i) is void ) ; ::_thesis: degree (Skeleton_of (KX,i)) <= degree KX
then  ( KX is empty-membered or Skeleton_of (KX,i) is empty-membered ) ;
then  degree (Skeleton_of (KX,i)) = - 1 by Th22;
hence  degree (Skeleton_of (KX,i)) <= degree KX by Th23; ::_thesis: verum
end;
supposeA1: ( not KX is void & KX is finite-degree & not Skeleton_of (KX,i) is void ) ; ::_thesis: degree (Skeleton_of (KX,i)) <= degree KX
then reconsider d = degree KX as Integer ;
now__::_thesis:_for_s_being_finite_Subset_of_(Skeleton_of_(KX,i))_st_s_is_simplex-like_holds_
card_s_<=_d_+_1
let s be finite Subset of (Skeleton_of (KX,i)); ::_thesis: ( s is simplex-like implies card s <= d + 1 )
assume  s is simplex-like ; ::_thesis: card s <= d + 1
then  s in subset-closed_closure_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) by PRE_TOPC:def_2;
then consider a being set  such that
A2: s c= a and
A3: a in the_subsets_with_limited_card ((i + 1), the topology of KX) by Th2;
A4: a in the topology of KX by A3, Def2;
reconsider a = a as finite Subset of KX by A3;
 card s c= card a by A2, CARD_1:11;
then A5: card s <= card a by NAT_1:39;
 ( a is simplex-like & not KX is void ) by A4, PENCIL_1:def_4, PRE_TOPC:def_2;
then  card a <= d + 1 by Th25;
hence  card s <= d + 1 by A5, XXREAL_0:2; ::_thesis: verum
end;
hence  degree (Skeleton_of (KX,i)) <= degree KX by A1, Th25; ::_thesis: verum
end;
supposeA6: not KX is finite-degree ; ::_thesis: degree (Skeleton_of (KX,i)) <= degree KX
 not KX is void
proof
assume  KX is void ; ::_thesis: contradiction
then  KX is empty-membered ;
hence  contradiction by A6; ::_thesis: verum
end;
then  degree KX = +infty by A6, Def12;
hence  degree (Skeleton_of (KX,i)) <= degree KX by XXREAL_0:3; ::_thesis: verum
end;
end;
end;

theorem :: SIMPLEX0:44
for X being set
for i being Integer
for KX being SimplicialComplexStr of X st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i
proof
let X be set ; ::_thesis: for i being Integer
for KX being SimplicialComplexStr of X st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i
let i be Integer; ::_thesis: for KX being SimplicialComplexStr of X st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i
let KX be SimplicialComplexStr of X; ::_thesis: ( - 1 <= i implies degree (Skeleton_of (KX,i)) <= i )
set swlc = the_subsets_with_limited_card ((i + 1), the topology of KX);
set S = Skeleton_of (KX,i);
assume A1: - 1 <= i ; ::_thesis: degree (Skeleton_of (KX,i)) <= i
then  (- 1) + 1 <= i + 1 by XREAL_1:6;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;
now__::_thesis:_for_A_being_finite_Subset_of_(Skeleton_of_(KX,i))_st_A_is_simplex-like_holds_
card_A_<=_i_+_1
let A be finite Subset of (Skeleton_of (KX,i)); ::_thesis: ( A is simplex-like implies card A <= i + 1 )
assume  A is simplex-like ; ::_thesis: card A <= i + 1
then  A in the topology of (Skeleton_of (KX,i)) by PRE_TOPC:def_2;
then consider x being set  such that
A2: ( A c= x & x in the_subsets_with_limited_card ((i + 1), the topology of KX) ) by Th2;
 ( card x c= card (i + 1) & card A c= card x ) by A2, Def2, CARD_1:11;
then A3: card A c= card i1 by XBOOLE_1:1;
 card (card A) = card A ;
hence  card A <= i + 1 by A3, NAT_1:40; ::_thesis: verum
end;
hence  degree (Skeleton_of (KX,i)) <= i by A1, Th25; ::_thesis: verum
end;

theorem :: SIMPLEX0:45
for X being set
for i being Integer
for KX being SimplicialComplexStr of X st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds
degree KX <= i
proof
let X be set ; ::_thesis: for i being Integer
for KX being SimplicialComplexStr of X st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds
degree KX <= i
let i be Integer; ::_thesis: for KX being SimplicialComplexStr of X st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds
degree KX <= i
let KX be SimplicialComplexStr of X; ::_thesis: ( - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) implies degree KX <= i )
assume A1: - 1 <= i ; ::_thesis: ( not Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) or degree KX <= i )
percases ( KX is empty-membered or KX is with_non-empty_element ) ;
suppose KX is empty-membered ; ::_thesis: ( not Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) or degree KX <= i )
hence  ( not Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) or degree KX <= i ) by A1, Th22; ::_thesis: verum
end;
supposeA2: KX is with_non-empty_element ; ::_thesis: ( not Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) or degree KX <= i )
 (- 1) + 1 <= i + 1 by A1, XREAL_1:6;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;
assume A3: Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) ; ::_thesis: degree KX <= i
A4: now__::_thesis:_for_S_being_finite_Subset_of_KX_st_S_is_simplex-like_holds_
card_S_<=_i1
let S be finite Subset of KX; ::_thesis: ( S is simplex-like implies card S <= i1 )
assume  S is simplex-like ; ::_thesis: card S <= i1
then  S in subset-closed_closure_of (the_subsets_with_limited_card (i1, the topology of KX)) by A3, PRE_TOPC:def_2;
then consider y being set  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 i1 by XBOOLE_1:1;
 card S = card (card S) ;
hence  card S <= i1 by A6, NAT_1:40; ::_thesis: verum
end;
 for x being set st x in the topology of KX holds
x is finite by A3;
then  the_family_of KX is finite-membered by FINSET_1:def_6;
then  KX is finite-membered by MATROID0:def_6;
hence  degree KX <= i by A2, A4, Th25; ::_thesis: verum
end;
end;
end;

theorem :: SIMPLEX0:46
for X being set
for i being Integer
for KX being SimplicialComplexStr of X st KX is subset-closed & degree KX <= i holds
Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #)
proof
let X be set ; ::_thesis: for i being Integer
for KX being SimplicialComplexStr of X st KX is subset-closed & degree KX <= i holds
Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #)
let i be Integer; ::_thesis: for KX being SimplicialComplexStr of X st KX is subset-closed & degree KX <= i holds
Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #)
let KX be SimplicialComplexStr of X; ::_thesis: ( KX is subset-closed & degree KX <= i implies Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) )
assume that
A1: KX is subset-closed and
A2: degree KX <= i ; ::_thesis: Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #)
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 (Skeleton_of (KX,i))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of KX or x in the topology of (Skeleton_of (KX,i)) )
A6: (degree KX) + 1 <= i + 1 by A2, XXREAL_3:36;
assume A7: x in the topology of KX ; ::_thesis: x in the topology of (Skeleton_of (KX,i))
then reconsider A = x as finite Subset of KX by A4;
 ( A is simplex-like & not KX is void ) by A7, PENCIL_1:def_4, PRE_TOPC:def_2;
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 (card A) c= card (i + 1) by NAT_1:40;
then  A in the_subsets_with_limited_card ((i + 1), the topology of KX) by A7, Def2;
hence  x in the topology of (Skeleton_of (KX,i)) by Th2; ::_thesis: verum
end;
A8: the_subsets_with_limited_card ((i + 1), the topology of KX) c= the topology of KX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_subsets_with_limited_card ((i + 1), the topology of KX) or x in the topology of KX )
thus  ( not x in the_subsets_with_limited_card ((i + 1), the topology of KX) or x in the topology of KX ) by Def2; ::_thesis: verum
end;
 the_family_of KX is subset-closed by A1;
then  the topology of (Skeleton_of (KX,i)) c= the topology of KX by A8, Th3;
hence  Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

 Lm7:  for i being Integer
for K being non void subset-closed SimplicialComplexStr st - 1 <= i & i <= degree K holds
ex S being Simplex of K st card S = i + 1
proof
let i be Integer; ::_thesis: for K being non void subset-closed SimplicialComplexStr st - 1 <= i & i <= degree K holds
ex S being Simplex of K st card S = i + 1
let K be non void subset-closed SimplicialComplexStr; ::_thesis: ( - 1 <= i & i <= degree K implies ex S being Simplex of K st card S = i + 1 )
assume that
A1: - 1 <= i and
A2: i <= degree K ; ::_thesis: ex S being Simplex of K st card S = i + 1
 (- 1) + 1 <= i + 1 by A1, XREAL_1:6;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;
percases ( not K is finite-degree or K is finite-degree ) ;
supposeA3: not K is finite-degree ; ::_thesis: ex S being Simplex of K st card S = i + 1
percases ( not K is finite-membered or for n being Nat ex A being finite Subset of K st
( A is open & card A > n ) ) by A3, MATROID0:def_7;
suppose not K is finite-membered ; ::_thesis: ex S being Simplex of K st card S = i + 1
then  not the_family_of K is finite-membered by MATROID0:def_6;
then consider A being set  such that
A4: A in the_family_of K and
A5: A is infinite by FINSET_1:def_6;
 card i1 c= card A by A5;
then consider f being 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 ; ::_thesis: card R = i + 1
 R,i1 are_equipotent by A6, WELLORD2:def_4;
hence  card R = i + 1 by CARD_1:def_2; ::_thesis: verum
end;
suppose for n being Nat ex A being finite Subset of K st
( A is open & card A > n ) ; ::_thesis: ex S being Simplex of K st card S = i + 1
then consider A being finite Subset of K such that
A8: A is simplex-like and
A9: card A > i1 ;
 card i1 in card (card A) by A9, NAT_1:41;
then  card i1 c= card A by CARD_1:3;
then consider f being 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, PRE_TOPC:def_2;
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 ; ::_thesis: card R = i + 1
 R,i1 are_equipotent by A10, WELLORD2:def_4;
hence  card R = i + 1 by CARD_1:def_2; ::_thesis: verum
end;
end;
end;
supposeA12: K is finite-degree ; ::_thesis: ex S being Simplex of K st card S = i + 1
then reconsider d = degree K as Integer ;
consider S being 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  i1 c= card s by A14, NAT_1:39;
then  card i1 c= card (card s) by CARD_1:41;
then consider f being 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, PRE_TOPC:def_2;
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 ; ::_thesis: card R = i + 1
 R,i1 are_equipotent by A15, WELLORD2:def_4;
hence  card R = i + 1 by CARD_1:def_2; ::_thesis: verum
end;
end;
end;

definition
let K be non void subset-closed SimplicialComplexStr;
let i be real number ;
assume B1: i is integer ;
mode Simplex of i,K ->  finite Simplex of K means :Def18: :: SIMPLEX0:def 18
 card it = i + 1 if ( - 1 <= i & i <= degree K )
otherwise it is empty ;
existence
 ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) )
proof
A1: now__::_thesis:_(_(_-_1_>_i_or_i_>_degree_K_)_implies_ex_S_being_Simplex_of_K_st_
(_(_-_1_<=_i_&_i_<=_degree_K_implies_ex_b2_being_finite_Simplex_of_K_st_card_b2_=_i_+_1_)_&_(_(_not_-_1_<=_i_or_not_i_<=_degree_K_)_implies_ex_b2_being_finite_Simplex_of_K_st_b2_is_empty_)_)_)
reconsider S = {} K as Simplex of K ;
assume A2: ( - 1 > i or i > degree K ) ; ::_thesis: ex S being Simplex of K st
( ( - 1 <= i & i <= degree K implies ex b2 being finite Simplex of K st card b2 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b2 being finite Simplex of K st b2 is empty ) )
take S = S; ::_thesis: ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) )
 S is empty ;
hence  ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) ) by A2; ::_thesis: verum
end;
now__::_thesis:_(_-_1_<=_i_&_i_<=_degree_K_implies_ex_S_being_Simplex_of_K_st_
(_(_-_1_<=_i_&_i_<=_degree_K_implies_ex_b2_being_finite_Simplex_of_K_st_card_b2_=_i_+_1_)_&_(_(_not_-_1_<=_i_or_not_i_<=_degree_K_)_implies_ex_b2_being_finite_Simplex_of_K_st_b2_is_empty_)_)_)
assume A3: ( - 1 <= i & i <= degree K ) ; ::_thesis: ex S being Simplex of K st
( ( - 1 <= i & i <= degree K implies ex b2 being finite Simplex of K st card b2 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b2 being finite Simplex of K st b2 is empty ) )
then consider S being Simplex of K such that
A4: card S = i + 1 by B1, Lm7;
take S = S; ::_thesis: ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) )
 S is finite by B1, A4;
hence  ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) ) by A3, A4; ::_thesis: verum
end;
hence  ( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) ) by A1; ::_thesis: verum
end;
correctness
consistency
for b1 being finite Simplex of K holds verum;
;
end;

:: deftheorem Def18 defines Simplex SIMPLEX0:def_18_:_
 for K being non void subset-closed SimplicialComplexStr
for i being real number st i is integer holds
for b3 being finite Simplex of K holds
( ( - 1 <= i & i <= degree K implies ( b3 is Simplex of i,K iff card b3 = i + 1 ) ) & ( ( not - 1 <= i or not i <= degree K ) implies ( b3 is Simplex of i,K iff b3 is empty ) ) );

registration
let K be non void subset-closed SimplicialComplexStr;
cluster  ->  empty for Simplex of - 1,K;
coherence
 for b1 being Simplex of - 1,K holds b1 is empty
proof
let S be Simplex of - 1,K; ::_thesis: S is empty
 - 1 <= degree K by Th23;
then  card S = (- 1) + 1 by Def18
.= 0 ;
hence  S is empty ; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:47
for i being Integer
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of i,K st not S is empty holds
i is natural
proof
let i be Integer; ::_thesis: for K being non void subset-closed SimplicialComplexStr
for S being Simplex of i,K st not S is empty holds
i is natural
let K be non void subset-closed SimplicialComplexStr; ::_thesis: for S being Simplex of i,K st not S is empty holds
i is natural
let S be Simplex of i,K; ::_thesis: ( not S is empty implies i is natural )
assume  not S is empty ; ::_thesis: i is natural
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  i is natural ; ::_thesis: verum
end;

theorem :: SIMPLEX0:48
for K being non void subset-closed SimplicialComplexStr
for S being finite Simplex of K holds S is Simplex of (card S) - 1,K
proof
let K be non void subset-closed SimplicialComplexStr; ::_thesis: for S being finite Simplex of K holds S is Simplex of (card S) - 1,K
let S be finite Simplex of K; ::_thesis: S is Simplex of (card S) - 1,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  S is Simplex of (card S) - 1,K by A1, Def18; ::_thesis: verum
end;

theorem :: SIMPLEX0:49
for D being non empty set
for K being non void subset-closed SimplicialComplexStr of D
for S being non void SubSimplicialComplex of K
for i being Integer
for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K
proof
let D be non empty set ; ::_thesis: for K being non void subset-closed SimplicialComplexStr of D
for S being non void SubSimplicialComplex of K
for i being Integer
for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K
let K be non void subset-closed SimplicialComplexStr of D; ::_thesis: for S being non void SubSimplicialComplex of K
for i being Integer
for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K
let S be non void SubSimplicialComplex of K; ::_thesis: for i being Integer
for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K
let i be Integer; ::_thesis: for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K
let A be Simplex of i,S; ::_thesis: ( ( not A is empty or i <= degree S or degree S = degree K ) implies A is Simplex of i,K )
assume A1: ( not A is empty or i <= degree S or degree S = degree K ) ; ::_thesis: A is Simplex of i,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;
percases ( not A is empty or i <= degree S or degree S = degree K ) by A1;
supposeA3: not A is empty ; ::_thesis: A is Simplex of i,K
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  A is Simplex of i,K by A6, A4, Def18; ::_thesis: verum
end;
supposeA7: i <= degree S ; ::_thesis: A is Simplex of i,K
then A8: i <= degree K by A2, XXREAL_0:2;
percases ( - 1 <= i or - 1 > i ) ;
supposeA9: - 1 <= i ; ::_thesis: A is Simplex of i,K
then  card B = i + 1 by A7, Def18;
hence  A is Simplex of i,K by A8, A9, Def18; ::_thesis: verum
end;
supposeA10: - 1 > i ; ::_thesis: A is Simplex of i,K
then  B is empty by Def18;
hence  A is Simplex of i,K by A10, Def18; ::_thesis: verum
end;
end;
end;
supposeA11: degree S = degree K ; ::_thesis: A is Simplex of i,K
percases ( ( - 1 <= i & i <= degree S ) or - 1 > i or i > degree S ) ;
supposeA12: ( - 1 <= i & i <= degree S ) ; ::_thesis: A is Simplex of i,K
then  card B = i + 1 by Def18;
hence  A is Simplex of i,K by A11, A12, Def18; ::_thesis: verum
end;
supposeA13: ( - 1 > i or i > degree S ) ; ::_thesis: A is Simplex of i,K
then  B is empty by Def18;
hence  A is Simplex of i,K by A11, A13, Def18; ::_thesis: verum
end;
end;
end;
end;
end;

definition
let K be non void subset-closed SimplicialComplexStr;
let i be real number ;
assume that
B1: i is integer and
B2: i <= degree K ;
let S be Simplex of i,K;
mode Face of S ->  Simplex of max ((i - 1),(- 1)),K means :Def19: :: SIMPLEX0:def 19
it c= S;
existence
 ex b1 being Simplex of max ((i - 1),(- 1)),K st b1 c= S
proof
percases ( i < 0 or i >= 0 ) ;
suppose i < 0 ; ::_thesis: ex b1 being Simplex of max ((i - 1),(- 1)),K st b1 c= S
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 ; ::_thesis: F c= S
thus  F c= S by XBOOLE_1:2; ::_thesis: verum
end;
supposeA1: i >= 0 ; ::_thesis: ex b1 being Simplex of max ((i - 1),(- 1)),K st b1 c= S
then A2: card S = i + 1 by B1, B2, Def18;
then  not S is empty by A1;
then consider x being set  such that
A3: x in S by XBOOLE_0:def_1;
reconsider I = i as Element of NAT by B1, A1, INT_1:3;
 i - 1 <= (degree K) - 0 by B2, XXREAL_3:37;
then A4: i - 1 <= degree K by XXREAL_3:4;
reconsider Sx = S \ {x} as Simplex of K ;
A5: card Sx = (I - 1) + 1 by A2, A3, STIRL2_1:55;
A6: i - 1 >= 0 - 1 by A1, XREAL_1:6;
then  max ((i - 1),(- 1)) = i - 1 by XXREAL_0:def_10;
then reconsider Sx = Sx as Simplex of max ((i - 1),(- 1)),K by A4, A5, A6, Def18;
take  Sx ; ::_thesis: Sx c= S
thus  Sx c= S by XBOOLE_1:36; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def19 defines Face SIMPLEX0:def_19_:_
 for K being non void subset-closed SimplicialComplexStr
for i being real number st i is integer & i <= degree K holds
for S being Simplex of i,K
for b4 being Simplex of max ((i - 1),(- 1)),K holds
( b4 is Face of S iff b4 c= S );

theorem :: SIMPLEX0:50
for X being set
for n being Nat
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
proof
let X be set ; ::_thesis: for n being Nat
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
let n be Nat; ::_thesis: for K being non void subset-closed SimplicialComplexStr
for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
let K be non void subset-closed SimplicialComplexStr; ::_thesis: for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
let S be Simplex of n,K; ::_thesis: ( n <= degree K implies ( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) ) )
assume A1: n <= degree K ; ::_thesis: ( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
 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  ::_thesis: ( ex x being set st
( x in S & S \ {x} = X ) implies X is Face of S )
assume  X is Face of S ; ::_thesis: ex x being set st
( x in S & S \ {x} = X )
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 being set  such that
A7: S \ f = {x} by CARD_2:42;
take x = x; ::_thesis: ( x in S & S \ {x} = X )
 x in {x} by TARSKI:def_1;
hence  x in S by A7, XBOOLE_0:def_5; ::_thesis: S \ {x} = X
thus S \ {x} = f /\ S by A7, XBOOLE_1:48
.= X by A6, XBOOLE_1:28 ; ::_thesis: verum
end;
given x being set  such that A8: x in S and
A9: S \ {x} = X ; ::_thesis: X is Face of S
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  X is Face of S by A1, A4, A10, Def19; ::_thesis: verum
end;

begin

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let P be Function;
func subdivision (P,KX) ->  strict SimplicialComplexStr of X means :Def20: :: SIMPLEX0:def 20
( [#] it = [#] KX & ( for A being Subset of it holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) );
existence
 ex b1 being strict SimplicialComplexStr of X st
( [#] b1 = [#] KX & ( for A being Subset of b1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) )
proof
defpred S1[ set ] means  ex S being c=-linear finite simplex-like Subset-Family of KX st $1 = P .: S;
set SS =  {  A where A is Subset of KX : S1[A]  }  ;
  {  A where A is Subset of KX : S1[A]  }  c= bool the carrier of KX
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of KX : S1[A]  }  or x in bool the carrier of KX )
assume  x in  {  A where A is Subset of KX : S1[A]  }  ; ::_thesis: x in bool the carrier of KX
then  ex A being Subset of KX st
( x = A & S1[A] ) ;
hence  x in bool the carrier of KX ; ::_thesis: verum
end;
then reconsider SS =  {  A where A is Subset of KX : S1[A]  }  as Subset-Family of KX ;
set PP = TopStruct(# the carrier of KX,SS #);
 ( [#] TopStruct(# the carrier of KX,SS #) = [#] KX & [#] KX c= X ) by Def9;
then reconsider PP = TopStruct(# the carrier of KX,SS #) as strict SimplicialComplexStr of X by Def9;
take  PP ; ::_thesis: ( [#] PP = [#] KX & ( for A being Subset of PP holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) )
thus  [#] PP = [#] KX ; ::_thesis: for A being Subset of PP holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S )
let A be Subset of PP; ::_thesis: ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S )
hereby  ::_thesis: ( ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S implies A is simplex-like )
assume  A is simplex-like ; ::_thesis: S1[A]
then  A in SS by PRE_TOPC:def_2;
then  ex B being Subset of KX st
( B = A & S1[B] ) ;
hence  S1[A] ; ::_thesis: verum
end;
assume  S1[A] ; ::_thesis: A is simplex-like
then  A in SS ;
hence  A is simplex-like by PRE_TOPC:def_2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict SimplicialComplexStr of X st [#] b1 = [#] KX & ( for A being Subset of b1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] b2 = [#] KX & ( for A being Subset of b2 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) holds
b1 = b2
proof
let P1, P2 be strict SimplicialComplexStr of X; ::_thesis: ( [#] P1 = [#] KX & ( for A being Subset of P1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] P2 = [#] KX & ( for A being Subset of P2 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) implies P1 = P2 )
assume that
A1: [#] P1 = [#] KX and
A2: for A being Subset of P1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) and
A3: [#] P2 = [#] KX and
A4: for A being Subset of P2 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ; ::_thesis: P1 = P2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_topology_of_P1_implies_x_in_the_topology_of_P2_)_&_(_x_in_the_topology_of_P2_implies_x_in_the_topology_of_P1_)_)
let x be set ; ::_thesis: ( ( x in the topology of P1 implies x in the topology of P2 ) & ( x in the topology of P2 implies x in the topology of P1 ) )
hereby  ::_thesis: ( x in the topology of P2 implies x in the topology of P1 )
assume A5: x in the topology of P1 ; ::_thesis: x in the topology of P2
then reconsider A = x as Subset of P1 ;
reconsider B = A as Subset of P2 by A1, A3;
 A is simplex-like by A5, PRE_TOPC:def_2;
then  ex S being 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 by PRE_TOPC:def_2; ::_thesis: verum
end;
assume A6: x in the topology of P2 ; ::_thesis: x in the topology of P1
then reconsider A = x as Subset of P2 ;
reconsider B = A as Subset of P1 by A1, A3;
 A is simplex-like by A6, PRE_TOPC:def_2;
then  ex S being 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 by PRE_TOPC:def_2; ::_thesis: verum
end;
hence  P1 = P2 by A1, A3, TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines subdivision SIMPLEX0:def_20_:_
 for X being set
for KX being SimplicialComplexStr of X
for P being Function
for b4 being strict SimplicialComplexStr of X holds
( b4 = subdivision (P,KX) iff ( [#] b4 = [#] KX & ( for A being Subset of b4 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ) );

registration
let X be set ;
let KX be SimplicialComplexStr of X;
let P be Function;
cluster subdivision (P,KX) ->  strict subset-closed finite-membered with_empty_element ;
coherence
 ( not subdivision (P,KX) is with_non-empty_elements & subdivision (P,KX) is subset-closed & subdivision (P,KX) is finite-membered )
proof
set PP = subdivision (P,KX);
set S = the empty c=-linear simplex-like Subset-Family of KX;
 P .: the empty c=-linear simplex-like Subset-Family of KX = {} KX ;
then  {} (subdivision (P,KX)) is simplex-like by Def20;
then  {} in the topology of (subdivision (P,KX)) by PRE_TOPC:def_2;
then  the topology of (subdivision (P,KX)) is with_empty_element ;
hence  subdivision (P,KX) is with_empty_element by Def8; ::_thesis: ( subdivision (P,KX) is subset-closed & subdivision (P,KX) is finite-membered )
thus  subdivision (P,KX) is subset-closed ::_thesis: subdivision (P,KX) is finite-membered
proof
let x be set ; :: according to CLASSES1:def_1,MATROID0:def_3 ::_thesis: for b1 being set holds
( not x in the_family_of (subdivision (P,KX)) or not b1 c= x or b1 in the_family_of (subdivision (P,KX)) )
let y be set ; ::_thesis: ( not x in the_family_of (subdivision (P,KX)) or not y c= x or y in the_family_of (subdivision (P,KX)) )
assume that
A1: x in the_family_of (subdivision (P,KX)) and
A2: y c= x ; ::_thesis: y in the_family_of (subdivision (P,KX))
reconsider X = x, Y = y as Subset of (subdivision (P,KX)) by A1, A2, XBOOLE_1:1;
 X is simplex-like by A1, PRE_TOPC:def_2;
then consider S being c=-linear finite simplex-like Subset-Family of KX such that
A3: X = P .: S by Def20;
set S1 =  {  A where A is Subset of KX : ( A in S & P . A in Y )  }  ;
  {  A where A is Subset of KX : ( A in S & P . A in Y )  }  c= S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of KX : ( A in S & P . A in Y )  }  or x in S )
assume  x in  {  A where A is Subset of KX : ( A in S & P . A in Y )  }  ; ::_thesis: x in S
then  ex A being Subset of KX st
( A = x & A in S & P . A in Y ) ;
hence  x in S ; ::_thesis: verum
end;
then reconsider S1 =  {  A where A is Subset of KX : ( A in S & P . A in Y )  }  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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P .: S1 or x in Y )
assume  x in P .: S1 ; ::_thesis: x in Y
then consider y being set  such that
 y in dom P and
A5: y in S1 and
A6: P . y = x by FUNCT_1:def_6;
 ex B being Subset of KX st
( y = B & B in S & P . B in Y ) by A5;
hence  x in Y by A6; ::_thesis: verum
end;
 Y c= P .: S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in P .: S1 )
assume A7: x in Y ; ::_thesis: x in P .: S1
then consider y being set  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  x in P .: S1 by A8, A10, FUNCT_1:def_6; ::_thesis: verum
end;
then  P .: S1 = Y by A4, XBOOLE_0:def_10;
then  Y is simplex-like by Def20;
hence  y in the_family_of (subdivision (P,KX)) by PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to FINSET_1:def_6,MATROID0:def_6 ::_thesis: ( not x in the_family_of (subdivision (P,KX)) or x is finite )
assume A11: x in the_family_of (subdivision (P,KX)) ; ::_thesis: x is finite
then reconsider A = x as Subset of (subdivision (P,KX)) ;
 A is simplex-like by A11, PRE_TOPC:def_2;
then  ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S by Def20;
hence  x is finite ; ::_thesis: verum
end;
end;

registration
let X be set ;
let KX be void SimplicialComplexStr of X;
let P be Function;
cluster subdivision (P,KX) ->  strict empty-membered ;
coherence
 subdivision (P,KX) is empty-membered
proof
set PP = subdivision (P,KX);
assume  subdivision (P,KX) is with_non-empty_element ; ::_thesis: contradiction
then  the topology of (subdivision (P,KX)) is with_non-empty_element by Def7;
then consider x being non empty set  such that
A1: x in the topology of (subdivision (P,KX)) by SETFAM_1:def_10;
reconsider A = x as Simplex of (subdivision (P,KX)) by A1, PRE_TOPC:def_2;
consider S being 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  not S /\ (dom P) is empty ;
then consider y being set  such that
A3: y in S /\ (dom P) by XBOOLE_0:def_1;
A4: y in S by A3, XBOOLE_0:def_4;
reconsider y = y as Subset of KX by A3;
 y is simplex-like by A4, TOPS_2:def_1;
then  y in the topology of KX by PRE_TOPC:def_2;
hence  contradiction by PENCIL_1:def_4; ::_thesis: verum
end;
end;

theorem Th51: :: SIMPLEX0:51
for X being set
for KX being SimplicialComplexStr of X
for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1
let P be Function; ::_thesis: degree (subdivision (P,KX)) <= (degree KX) + 1
set PP = subdivision (P,KX);
percases ( KX is void or ( not KX is void & not KX is finite-degree ) or ( not KX is void & KX is finite-degree ) ) ;
suppose KX is void ; ::_thesis: degree (subdivision (P,KX)) <= (degree KX) + 1
then  ( KX is empty-membered & degree (subdivision (P,KX)) = - 1 ) by Th22;
hence  degree (subdivision (P,KX)) <= (degree KX) + 1 ; ::_thesis: verum
end;
supposeA1: ( not KX is void & not KX is finite-degree ) ; ::_thesis: degree (subdivision (P,KX)) <= (degree KX) + 1
A2: ( degree (subdivision (P,KX)) <= +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  degree (subdivision (P,KX)) <= (degree KX) + 1 by A2, XXREAL_0:2; ::_thesis: verum
end;
supposeA3: ( not KX is void & KX is finite-degree ) ; ::_thesis: degree (subdivision (P,KX)) <= (degree KX) + 1
then reconsider d = degree KX as Integer ;
reconsider d1 = d + 1 as Nat by A3;
 for A being finite Subset of (subdivision (P,KX)) st A is simplex-like holds
card A <= (d + 1) + 1
proof
let A be finite Subset of (subdivision (P,KX)); ::_thesis: ( A is simplex-like implies card A <= (d + 1) + 1 )
assume  A is simplex-like ; ::_thesis: card A <= (d + 1) + 1
then consider S being 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  card A c= card (S /\ (dom P)) by CARD_1:67;
then A5: card A <= card (S /\ (dom P)) by NAT_1:39;
 (S /\ (dom P)) \ {{}} c= S by XBOOLE_1:18, XBOOLE_1:36;
then reconsider SP = (S /\ (dom P)) \ {{}} as c=-linear finite simplex-like Subset-Family of KX by TOPS_2:11;
 SP \/ {{}} = (S /\ (dom P)) \/ {{}} by XBOOLE_1:39;
then A6: ( card {{}} = 1 & card (S /\ (dom P)) <= card (SP \/ {{}}) ) by CARD_1:30, NAT_1:43, XBOOLE_1:7;
 card (SP \/ {{}}) <= (card SP) + (card {{}}) by CARD_2:43;
then A7: card (S /\ (dom P)) <= (card SP) + 1 by A6, XXREAL_0:2;
percases ( SP is empty or not SP is empty ) ;
supposeA8: SP is empty ; ::_thesis: card A <= (d + 1) + 1
 0 + 1 <= d1 + 1 by XREAL_1:6;
then  card (S /\ (dom P)) <= d1 + 1 by A6, A8, XXREAL_0:2;
hence  card A <= (d + 1) + 1 by A5, XXREAL_0:2; ::_thesis: verum
end;
supposeA9: not SP is empty ; ::_thesis: card A <= (d + 1) + 1
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 by SETFAM_1:def_8;
then A11: card SP c= card (union SP) by Th10;
reconsider uSP = uSP as finite Subset of KX by A3;
 card uSP <= d1 by A3, A10, Th25;
then  card uSP c= d1 by NAT_1:39;
then  card SP c= d1 by A11, XBOOLE_1:1;
then  card SP <= d1 by NAT_1:39;
then  (card SP) + 1 <= d1 + 1 by XREAL_1:6;
then  card (S /\ (dom P)) <= d1 + 1 by A7, XXREAL_0:2;
hence  card A <= (d + 1) + 1 by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  degree (subdivision (P,KX)) <= (degree KX) + 1 by Th25; ::_thesis: verum
end;
end;
end;

theorem Th52: :: SIMPLEX0:52
for X being set
for KX being SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX
let P be Function; ::_thesis: ( dom P is with_non-empty_elements implies degree (subdivision (P,KX)) <= degree KX )
assume A1: dom P is with_non-empty_elements ; ::_thesis: degree (subdivision (P,KX)) <= degree KX
set PP = subdivision (P,KX);
percases ( not KX is finite-degree or KX is finite-degree ) ;
supposeA2: not KX is finite-degree ; ::_thesis: degree (subdivision (P,KX)) <= degree KX
 not KX is void
proof
assume  KX is void ; ::_thesis: contradiction
then  KX is empty-membered ;
hence  contradiction by A2; ::_thesis: verum
end;
then  degree KX = +infty by A2, Def12;
hence  degree (subdivision (P,KX)) <= degree KX by XXREAL_0:3; ::_thesis: verum
end;
supposeA3: KX is finite-degree ; ::_thesis: degree (subdivision (P,KX)) <= degree KX
then reconsider d = degree KX as Integer ;
reconsider d1 = d + 1 as Nat by A3;
 for A being finite Subset of (subdivision (P,KX)) st A is simplex-like holds
card A <= d + 1
proof
let A be finite Subset of (subdivision (P,KX)); ::_thesis: ( A is simplex-like implies card A <= d + 1 )
assume  A is simplex-like ; ::_thesis: card A <= d + 1
then consider S being 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;
percases ( S /\ (dom P) is empty or not S /\ (dom P) is empty ) ;
suppose S /\ (dom P) is empty ; ::_thesis: card A <= d + 1
then  ( 0 <= d1 & A = {} ) by A5;
hence  card A <= d + 1 ; ::_thesis: verum
end;
supposeA6: not S /\ (dom P) is empty ; ::_thesis: card A <= d + 1
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 by PRE_TOPC:def_2;
 the_family_of KX is finite-membered by A3, MATROID0:def_6;
then reconsider uSP = uSP as finite Subset of KX by A9;
 not KX is void by A9, PENCIL_1:def_4;
then  card uSP <= d + 1 by A8, Th25;
then A10: card uSP c= 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, XBOOLE_1:1;
 card A c= card (S /\ (dom P)) by A5, CARD_1:67;
then  card A c= d1 by A11, XBOOLE_1:1;
hence  card A <= d + 1 by NAT_1:39; ::_thesis: verum
end;
end;
end;
hence  degree (subdivision (P,KX)) <= degree KX by Th25; ::_thesis: verum
end;
end;
end;

registration
let X be set ;
let KX be finite-degree SimplicialComplexStr of X;
let P be Function;
cluster subdivision (P,KX) ->  strict finite-degree ;
coherence
 subdivision (P,KX) is finite-degree
proof
assume  not subdivision (P,KX) is finite-degree ; ::_thesis: contradiction
then  ( (degree KX) + 1 in REAL & degree (subdivision (P,KX)) = +infty ) by Def12, XREAL_0:def_1;
hence  contradiction by Th51, XXREAL_0:9; ::_thesis: verum
end;
end;

registration
let X be set ;
let KX be finite-vertices SimplicialComplexStr of X;
let P be Function;
cluster subdivision (P,KX) ->  strict finite-vertices ;
coherence
 subdivision (P,KX) is finite-vertices
proof
reconsider V = Vertices KX as finite Subset of KX by Def5;
set PP = subdivision (P,KX);
set TOP = the topology of (subdivision (P,KX));
defpred S1[ set , set ] means P .: KX = X;
 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 being set st x in the topology of (subdivision (P,KX)) holds
ex y being set st
( y in bool (bool V) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the topology of (subdivision (P,KX)) implies ex y being set st
( y in bool (bool V) & S1[x,y] ) )
assume A3: x in the topology of (subdivision (P,KX)) ; ::_thesis: ex y being set st
( y in bool (bool V) & S1[x,y] )
reconsider X = x as Subset of (subdivision (P,KX)) by A3;
 X is simplex-like by A3, PRE_TOPC:def_2;
then consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: X = P .: S by Def20;
take  S ; ::_thesis: ( S in bool (bool V) & S1[x,S] )
 S c= the topology of KX
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in S or y in the topology of KX )
assume A5: y in S ; ::_thesis: y in the topology of KX
reconsider Y = y as Subset of KX by A5;
 Y is simplex-like by A5, TOPS_2:def_1;
hence  y in the topology of KX by PRE_TOPC:def_2; ::_thesis: verum
end;
then  S c= bool V by A1, XBOOLE_1:1;
hence  ( S in bool (bool V) & S1[x,S] ) by A4; ::_thesis: verum
end;
consider f being Function of the topology of (subdivision (P,KX)),(bool (bool V)) such that
A6: for x being set st x in the topology of (subdivision (P,KX)) holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in dom f and
A8: ( x2 in dom f & f . x1 = f . x2 ) ; ::_thesis: x1 = x2
thus x1 = P .: (f . x1) by A6, A7
.= x2 by A6, A8 ; ::_thesis: verum
end;
then A9: f is one-to-one by FUNCT_1:def_4;
 ( dom f = the topology of (subdivision (P,KX)) & rng f c= bool (bool V) ) by FUNCT_2:def_1;
then  card the topology of (subdivision (P,KX)) c= card (bool (bool V)) by A9, CARD_1:10;
then  the topology of (subdivision (P,KX)) is finite ;
hence  subdivision (P,KX) is finite-vertices by Th20; ::_thesis: verum
end;
end;

theorem :: SIMPLEX0:53
for X being set
for KX being subset-closed SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements & ( for n being Nat st n <= degree KX holds
ex S being 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 X be set ; ::_thesis: for KX being subset-closed SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements & ( for n being Nat st n <= degree KX holds
ex S being 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
let K be subset-closed SimplicialComplexStr of X; ::_thesis: for P being Function st dom P is with_non-empty_elements & ( for n being Nat st n <= degree K holds
ex S being 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 ) ) holds
degree (subdivision (P,K)) = degree K
let P be Function; ::_thesis: ( dom P is with_non-empty_elements & ( for n being Nat st n <= degree K holds
ex S being 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 ) ) implies degree (subdivision (P,K)) = degree K )
assume that
A1: dom P is with_non-empty_elements and
A2: for n being Nat st n <= degree K holds
ex S being 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 ) ; ::_thesis: degree (subdivision (P,K)) = degree K
set PP = subdivision (P,K);
A3: degree (subdivision (P,K)) <= degree K by A1, Th52;
A4: for n being Nat st n <= degree K holds
ex S being Simplex of (subdivision (P,K)) st card S = n + 1
proof
let n be Nat; ::_thesis: ( n <= degree K implies ex S being Simplex of (subdivision (P,K)) st card S = n + 1 )
A5: [#] K = [#] (subdivision (P,K)) by Def20;
assume  n <= degree K ; ::_thesis: ex S being Simplex of (subdivision (P,K)) st card S = n + 1
then consider A being 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;
 not A is empty by A7;
then consider S being Subset-Family of A such that
A12: ( S is with_non-empty_elements & S is c=-linear ) and
 A in S and
A13: card A = card S and
 for Z being set st Z in S & card Z <> 1 holds
ex x being set 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in BOOL A )
assume  x in S ; ::_thesis: x in BOOL A
then  x in (bool A) \ {{}} by A12, ZFMISC_1:56;
hence  x in BOOL A by ORDERS_1:def_2; ::_thesis: verum
end;
then  P .: S c= P .: (BOOL A) by RELAT_1:123;
then reconsider PS = P .: SS as Subset of (subdivision (P,K)) by A5, A9, XBOOLE_1:1;
A15: A in the_family_of K by A6, PRE_TOPC:def_2;
 SS is simplex-like
proof
let B be Subset of K; :: according to TOPS_2:def_1 ::_thesis: ( not B in SS or B is simplex-like )
assume  B in SS ; ::_thesis: B is simplex-like
then  B in the_family_of K by A15, CLASSES1:def_1;
hence  B is simplex-like by PRE_TOPC:def_2; ::_thesis: verum
end;
then  SS is c=-linear finite simplex-like Subset-Family of K by A7, A12, A13;
then reconsider PS = PS as Simplex of (subdivision (P,K)) 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  ex S being Simplex of (subdivision (P,K)) st card S = n + 1 ; ::_thesis: verum
end;
percases ( K is empty-membered or ( K is with_non-empty_element & K is finite-degree ) or ( not K is void & not K is finite-degree ) ) ;
supposeA16: K is empty-membered ; ::_thesis: degree (subdivision (P,K)) = degree K
A17: degree (subdivision (P,K)) >= - 1 by Th23;
 degree K = - 1 by A16, Th22;
hence  degree (subdivision (P,K)) = degree K by A3, A17, XXREAL_0:1; ::_thesis: verum
end;
supposeA18: ( K is with_non-empty_element & K is finite-degree ) ; ::_thesis: degree (subdivision (P,K)) = degree K
then reconsider d = degree K, dPP = degree (subdivision (P,K)) 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 = d as Element of NAT by INT_1:3;
 ex S being Simplex of (subdivision (P,K)) st card S = d + 1 by A4;
then  dPP + 1 >= d + 1 by A18, Def12;
then  dPP >= d by XREAL_1:6;
hence  degree (subdivision (P,K)) = degree K by A3, XXREAL_0:1; ::_thesis: verum
end;
suppose ( not K is void & not K is finite-degree ) ; ::_thesis: degree (subdivision (P,K)) = degree K
then A20: degree K = +infty by Def12;
 not subdivision (P,K) is finite-degree
proof
assume A21: subdivision (P,K) is finite-degree ; ::_thesis: contradiction
then reconsider d = (degree (subdivision (P,K))) + 1 as Nat ;
consider S being Subset of (subdivision (P,K)) such that
A22: S is simplex-like and
A23: card S = d by A21, Def12;
reconsider S = S as finite Subset of (subdivision (P,K)) by A22;
 ex S1 being Simplex of (subdivision (P,K)) 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; ::_thesis: verum
end;
hence  degree (subdivision (P,K)) = degree K by A20, Def12; ::_thesis: verum
end;
end;
end;

theorem Th54: :: SIMPLEX0:54
for X, Y, Z being set
for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX)
proof
let X, Y, Z be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX)
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function st Y c= Z holds
subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX)
let P be Function; ::_thesis: ( Y c= Z implies subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX) )
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 ; ::_thesis: subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX)
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: [#] (subdivision ((P | Y),KX)) = [#] KX by Def20;
hence  [#] (subdivision ((P | Y),KX)) c= [#] (subdivision ((P | Z),KX)) by Def20; :: according to SIMPLEX0:def_13 ::_thesis: the topology of (subdivision ((P | Y),KX)) c= the topology of (subdivision ((P | Z),KX))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision ((P | Y),KX)) or x in the topology of (subdivision ((P | Z),KX)) )
assume  x in the topology of (subdivision ((P | Y),KX)) ; ::_thesis: x in the topology of (subdivision ((P | Z),KX))
then reconsider A = x as Simplex of (subdivision ((P | Y),KX)) by PRE_TOPC:def_2;
 [#] (subdivision ((P | Z),KX)) = [#] KX by Def20;
then reconsider B = A as Subset of (subdivision ((P | Z),KX)) by A4;
consider S being 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 by XBOOLE_1:1;
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  x in the topology of (subdivision ((P | Z),KX)) by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem :: SIMPLEX0:55
for X, Y being set
for KX being SimplicialComplexStr of X
for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision ((P | Y),KX) = subdivision (P,KX)
proof
let X, Y be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision ((P | Y),KX) = subdivision (P,KX)
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision ((P | Y),KX) = subdivision (P,KX)
let P be Function; ::_thesis: ( (dom P) /\ the topology of KX c= Y implies subdivision ((P | Y),KX) = subdivision (P,KX) )
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: ( [#] (subdivision ((P | Y),KX)) = [#] KX & [#] (subdivision (P,KX)) = [#] KX ) by Def20;
assume A3: (dom P) /\ the topology of KX c= Y ; ::_thesis: subdivision ((P | Y),KX) = subdivision (P,KX)
A4: the topology of (subdivision (P,KX)) c= the topology of (subdivision ((P | Y),KX))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision (P,KX)) or x in the topology of (subdivision ((P | Y),KX)) )
assume  x in the topology of (subdivision (P,KX)) ; ::_thesis: x in the topology of (subdivision ((P | Y),KX))
then reconsider A = x as Simplex of (subdivision (P,KX)) by PRE_TOPC:def_2;
reconsider B = A as Subset of (subdivision ((P | Y),KX)) by A2;
consider S being 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ (dom P) or x in Y )
assume A7: x in S /\ (dom P) ; ::_thesis: x in Y
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 by PRE_TOPC:def_2;
 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  x in Y by A3; ::_thesis: verum
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  x in the topology of (subdivision ((P | Y),KX)) by PRE_TOPC:def_2; ::_thesis: verum
end;
 ( P | (dom P) = P & P | Y = (P | Y) | (dom (P | Y)) ) ;
then  subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision (P,KX) by A1, Th54, RELAT_1:60;
then  the topology of (subdivision ((P | Y),KX)) c= the topology of (subdivision (P,KX)) by Def13;
hence  subdivision ((P | Y),KX) = subdivision (P,KX) by A2, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th56: :: SIMPLEX0:56
for X, Y, Z being set
for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX)
proof
let X, Y, Z be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX)
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function st Y c= Z holds
subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX)
let P be Function; ::_thesis: ( Y c= Z implies subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX) )
assume A1: Y c= Z ; ::_thesis: subdivision ((Y |` P),KX) is SubSimplicialComplex of subdivision ((Z |` P),KX)
set PZ = subdivision ((Z |` P),KX);
set PY = subdivision ((Y |` P),KX);
A2: [#] (subdivision ((Y |` P),KX)) = [#] KX by Def20;
hence  [#] (subdivision ((Y |` P),KX)) c= [#] (subdivision ((Z |` P),KX)) by Def20; :: according to SIMPLEX0:def_13 ::_thesis: the topology of (subdivision ((Y |` P),KX)) c= the topology of (subdivision ((Z |` P),KX))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision ((Y |` P),KX)) or x in the topology of (subdivision ((Z |` P),KX)) )
assume  x in the topology of (subdivision ((Y |` P),KX)) ; ::_thesis: x in the topology of (subdivision ((Z |` P),KX))
then reconsider A = x as Simplex of (subdivision ((Y |` P),KX)) by PRE_TOPC:def_2;
consider S being 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;
 [#] (subdivision ((Z |` P),KX)) = [#] KX by Def20;
then reconsider A = A as Subset of (subdivision ((Z |` P),KX)) by A2;
A5: (Z |` P) .: Sd c= (Y |` P) .: Sd
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Z |` P) .: Sd or y in (Y |` P) .: Sd )
assume  y in (Z |` P) .: Sd ; ::_thesis: y in (Y |` P) .: Sd
then consider x being set  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  y in (Y |` P) .: Sd by A7, A9, FUNCT_1:def_6; ::_thesis: verum
end;
 A = (Y |` P) .: Sd by A3, RELAT_1:112;
then  A = (Z |` P) .: Sd by A4, A5, XBOOLE_0:def_10;
then  A is simplex-like by Def20;
hence  x in the topology of (subdivision ((Z |` P),KX)) by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem :: SIMPLEX0:57
for X, Y being set
for KX being SimplicialComplexStr of X
for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
proof
let X, Y be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
let P be Function; ::_thesis: ( P .: the topology of KX c= Y implies subdivision ((Y |` P),KX) = subdivision (P,KX) )
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 subdivision (P,KX) by Th56, XBOOLE_1:17;
A1: ( [#] PY = [#] KX & [#] (subdivision (P,KX)) = [#] KX ) by Def20;
assume A2: P .: the topology of KX c= Y ; ::_thesis: subdivision ((Y |` P),KX) = subdivision (P,KX)
A3: the topology of (subdivision (P,KX)) c= the topology of PY
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision (P,KX)) or x in the topology of PY )
assume  x in the topology of (subdivision (P,KX)) ; ::_thesis: x in the topology of PY
then reconsider A = x as Simplex of (subdivision (P,KX)) by PRE_TOPC:def_2;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: A = P .: S by Def20;
reconsider A = A as Subset of PY by A1;
 S c= the topology of KX
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in S or y in the topology of KX )
assume A5: y in S ; ::_thesis: y in the topology of KX
reconsider y = y as Subset of KX by A5;
 y is simplex-like by A5, TOPS_2:def_1;
hence  y in the topology of KX by PRE_TOPC:def_2; ::_thesis: verum
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  x in the topology of PY by PRE_TOPC:def_2; ::_thesis: verum
end;
 the topology of PY c= the topology of (subdivision (P,KX)) by Def13;
hence  subdivision ((Y |` P),KX) = subdivision (P,KX) by A1, A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th58: :: SIMPLEX0:58
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
let SX be SubSimplicialComplex of KX; ::_thesis: for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
let P be Function; ::_thesis: subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
set PS = subdivision (P,SX);
set PK = subdivision (P,KX);
A1: [#] SX c= [#] KX by Def13;
A2: [#] (subdivision (P,KX)) = [#] KX by Def20;
hence  [#] (subdivision (P,SX)) c= [#] (subdivision (P,KX)) by A1, Def20; :: according to SIMPLEX0:def_13 ::_thesis: the topology of (subdivision (P,SX)) c= the topology of (subdivision (P,KX))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision (P,SX)) or x in the topology of (subdivision (P,KX)) )
assume  x in the topology of (subdivision (P,SX)) ; ::_thesis: x in the topology of (subdivision (P,KX))
then reconsider A = x as Simplex of (subdivision (P,SX)) by PRE_TOPC:def_2;
 [#] (subdivision (P,SX)) = [#] SX by Def20;
then reconsider B = A as Subset of (subdivision (P,KX)) by A1, A2, XBOOLE_1:1;
consider SS being 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; :: according to TOPS_2:def_1 ::_thesis: ( not C in SK or C is simplex-like )
assume A4: C in SK ; ::_thesis: C is simplex-like
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 by PRE_TOPC:def_2;
 the topology of SX c= the topology of KX by Def13;
hence  C is simplex-like by A5, PRE_TOPC:def_2; ::_thesis: verum
end;
then  B is simplex-like by A3, Def20;
hence  x in the topology of (subdivision (P,KX)) by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem :: SIMPLEX0:59
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let SX be SubSimplicialComplex of KX; ::_thesis: for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let P be Function; ::_thesis: for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
set PK = subdivision (P,KX);
reconsider PS = subdivision (P,SX) as strict SubSimplicialComplex of subdivision (P,KX) by Th58;
let A be Subset of (subdivision (P,KX)); ::_thesis: ( dom P c= the topology of SX & A = [#] SX implies subdivision (P,SX) = (subdivision (P,KX)) | A )
assume that
A1: dom P c= the topology of SX and
A2: A = [#] SX ; ::_thesis: subdivision (P,SX) = (subdivision (P,KX)) | A
now__::_thesis:_for_a_being_Subset_of_PS_st_a_in_the_topology_of_(subdivision_(P,KX))_holds_
a_is_simplex-like
let a be Subset of PS; ::_thesis: ( a in the topology of (subdivision (P,KX)) implies a is simplex-like )
assume  a in the topology of (subdivision (P,KX)) ; ::_thesis: a is simplex-like
then reconsider b = a as Simplex of (subdivision (P,KX)) by PRE_TOPC:def_2;
consider SS being 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, XBOOLE_1:1;
 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; :: according to TOPS_2:def_1 ::_thesis: ( not B in Sd or B is simplex-like )
assume  B in Sd ; ::_thesis: B is simplex-like
then  B in dom P by XBOOLE_0:def_4;
hence  B is simplex-like by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
 P .: SS = P .: Sd by RELAT_1:112;
hence  a is simplex-like by A3, A5, Def20; ::_thesis: verum
end;
then A6: PS is maximal by Def14;
 [#] PS = [#] SX by Def20;
hence  subdivision (P,SX) = (subdivision (P,KX)) | A by A2, A6, Def16; ::_thesis: verum
end;

theorem Th60: :: SIMPLEX0:60
for X being set
for P being Function
for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)
proof
let X be set ; ::_thesis: for P being Function
for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)
let P be Function; ::_thesis: for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)
let K1, K2 be SimplicialComplexStr of X; ::_thesis: ( TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) implies subdivision (P,K1) = subdivision (P,K2) )
assume A1: TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) ; ::_thesis: subdivision (P,K1) = subdivision (P,K2)
set P1 = subdivision (P,K1);
set P2 = subdivision (P,K2);
A2: ( [#] K1 = [#] (subdivision (P,K1)) & [#] K2 = [#] (subdivision (P,K2)) ) by Def20;
A3: the topology of (subdivision (P,K1)) c= the topology of (subdivision (P,K2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision (P,K1)) or x in the topology of (subdivision (P,K2)) )
assume A4: x in the topology of (subdivision (P,K1)) ; ::_thesis: x in the topology of (subdivision (P,K2))
then reconsider A = x as Subset of (subdivision (P,K1)) ;
reconsider A1 = A as Subset of (subdivision (P,K2)) by A1, A2;
 A is simplex-like by A4, PRE_TOPC:def_2;
then consider S being 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  x in the topology of (subdivision (P,K2)) by PRE_TOPC:def_2; ::_thesis: verum
end;
 the topology of (subdivision (P,K2)) c= the topology of (subdivision (P,K1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (subdivision (P,K2)) or x in the topology of (subdivision (P,K1)) )
assume A6: x in the topology of (subdivision (P,K2)) ; ::_thesis: x in the topology of (subdivision (P,K1))
then reconsider A = x as Subset of (subdivision (P,K2)) ;
reconsider A1 = A as Subset of (subdivision (P,K1)) by A1, A2;
 A is simplex-like by A6, PRE_TOPC:def_2;
then consider S being 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  x in the topology of (subdivision (P,K1)) by PRE_TOPC:def_2; ::_thesis: verum
end;
hence  subdivision (P,K1) = subdivision (P,K2) by A1, A2, A3, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let P be Function;
let n be Nat;
func subdivision (n,P,KX) ->  SimplicialComplexStr of X means :Def21: :: SIMPLEX0:def 21
 ex F being Function st
( F . 0 = KX & F . n = it & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) );
existence
 ex b1 being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
proof
defpred S1[ set , set ] means  for SX being 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 being set st x in bool (bool ([#] KX)) holds
ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in bool (bool ([#] KX)) implies ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] ) )
assume A2: x in bool (bool ([#] KX)) ; ::_thesis: ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
percases ( ex SX being SimplicialComplexStr of X st
( the topology of SX = x & [#] SX = [#] KX ) or for SX being SimplicialComplexStr of X holds
( the topology of SX <> x or [#] SX <> [#] KX ) ) ;
suppose ex SX being SimplicialComplexStr of X st
( the topology of SX = x & [#] SX = [#] KX ) ; ::_thesis: ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
then consider SX being SimplicialComplexStr of X such that
A3: the topology of SX = x and
A4: [#] SX = [#] KX ;
take T = the topology of (subdivision (P,SX)); ::_thesis: ( T in bool (bool ([#] KX)) & S1[x,T] )
 [#] (subdivision (P,SX)) = [#] SX by Def20;
hence  T in bool (bool ([#] KX)) by A4; ::_thesis: S1[x,T]
let SX1 be SimplicialComplexStr of X; ::_thesis: ( the topology of SX1 = x & [#] SX1 = [#] KX implies the topology of (subdivision (P,SX1)) = T )
assume A5: ( the topology of SX1 = x & [#] SX1 = [#] KX ) ; ::_thesis: the topology of (subdivision (P,SX1)) = T
 TopStruct(# the carrier of SX, the topology of SX #) = TopStruct(# the carrier of SX1, the topology of SX1 #) by A3, A4, A5;
hence  the topology of (subdivision (P,SX1)) = T by Th60; ::_thesis: verum
end;
supposeA6: for SX being SimplicialComplexStr of X holds
( the topology of SX <> x or [#] SX <> [#] KX ) ; ::_thesis: ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
take  x ; ::_thesis: ( x in bool (bool ([#] KX)) & S1[x,x] )
thus  ( x in bool (bool ([#] KX)) & S1[x,x] ) by A2, A6; ::_thesis: verum
end;
end;
end;
consider f being Function of (bool (bool ([#] KX))),(bool (bool ([#] KX))) such that
A7: for x being set st x in bool (bool ([#] KX)) holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
deffunc H1( set , set ) ->  set = f . $2;
consider g being Function such that
A8: ( dom g = NAT & g . 0 = the topology of KX & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_11();
defpred S2[ Nat] means ( ex SX being SimplicialComplexStr of X st
( the topology of SX = g . $1 & [#] SX = [#] KX & ( $1 > 0 implies SX is strict ) ) & ( for SX being 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: S2[ 0 ]
proof
thus  ex SX being SimplicialComplexStr of X st
( the topology of SX = g . 0 & [#] SX = [#] KX & ( 0 > 0 implies SX is strict ) ) by A8; ::_thesis: for SX being SimplicialComplexStr of X st the topology of SX = g . 0 & [#] SX = [#] KX holds
g . (0 + 1) = the topology of (subdivision (P,SX))
let SX be SimplicialComplexStr of X; ::_thesis: ( the topology of SX = g . 0 & [#] SX = [#] KX implies g . (0 + 1) = the topology of (subdivision (P,SX)) )
assume  ( the topology of SX = g . 0 & [#] SX = [#] KX ) ; ::_thesis: g . (0 + 1) = the topology of (subdivision (P,SX))
then  TopStruct(# the carrier of SX, the topology of SX #) = TopStruct(# the carrier of KX, the topology of KX #) by A8;
hence  g . (0 + 1) = the topology of (subdivision (P,SX)) by A9, Th60; ::_thesis: verum
end;
defpred S3[ set , set ] means  for k being Nat st k = $1 holds
( ( k = 0 implies $2 = KX ) & ( k > 0 implies for SF being Subset-Family of KX st SF = g . k holds
$2 = TopStruct(# the carrier of KX,SF #) ) );
A11: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
set k1 = k + 1;
given SX being SimplicialComplexStr of X such that A12: the topology of SX = g . k and
A13: [#] SX = [#] KX and
 ( k > 0 implies SX is strict ) ; ::_thesis: ( ex SX being SimplicialComplexStr of X st
( the topology of SX = g . k & [#] SX = [#] KX & not g . (k + 1) = the topology of (subdivision (P,SX)) ) or S2[k + 1] )
assume  for SX being SimplicialComplexStr of X st the topology of SX = g . k & [#] SX = [#] KX holds
g . (k + 1) = the topology of (subdivision (P,SX)) ; ::_thesis: S2[k + 1]
then A14: g . (k + 1) = the topology of (subdivision (P,SX)) by A12, A13;
 [#] (subdivision (P,SX)) = [#] KX by A13, Def20;
hence  ex SX being SimplicialComplexStr of X st
( the topology of SX = g . (k + 1) & [#] SX = [#] KX & ( k + 1 > 0 implies SX is strict ) ) by A14; ::_thesis: for SX being SimplicialComplexStr of X st the topology of SX = g . (k + 1) & [#] SX = [#] KX holds
g . ((k + 1) + 1) = the topology of (subdivision (P,SX))
let S1 be SimplicialComplexStr of X; ::_thesis: ( the topology of S1 = g . (k + 1) & [#] S1 = [#] KX implies g . ((k + 1) + 1) = the topology of (subdivision (P,S1)) )
assume A15: ( the topology of S1 = g . (k + 1) & [#] S1 = [#] KX ) ; ::_thesis: g . ((k + 1) + 1) = the topology of (subdivision (P,S1))
 g . ((k + 1) + 1) = f . (g . (k + 1)) by A8;
hence  g . ((k + 1) + 1) = the topology of (subdivision (P,S1)) by A7, A15; ::_thesis: verum
end;
A16: for k being Nat holds S2[k] from NAT_1:sch_2(A10, A11);
A17: for x being set st x in NAT holds
ex y being set st S3[x,y]
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S3[x,y] )
assume  x in NAT ; ::_thesis: ex y being set st S3[x,y]
then reconsider m = x as Nat ;
percases ( m = 0 or m > 0 ) ;
supposeA18: m = 0 ; ::_thesis: ex y being set st S3[x,y]
take  KX ; ::_thesis: S3[x,KX]
thus  S3[x,KX] by A18; ::_thesis: verum
end;
supposeA19: m > 0 ; ::_thesis: ex y being set st S3[x,y]
consider K1 being 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 #) ; ::_thesis: S3[x, TopStruct(# the carrier of KX,TOP #)]
thus  S3[x, TopStruct(# the carrier of KX,TOP #)] by A19, A20; ::_thesis: verum
end;
end;
end;
consider h being Function such that
A22: ( dom h = NAT & ( for x being set st x in NAT holds
S3[x,h . x] ) ) from CLASSES1:sch_1(A17);
A23: 0 in NAT by ORDINAL1:def_12;
then A24: h . 0 = KX by A22;
A25: for k being Nat
for K1 being SimplicialComplexStr of X st h . k = K1 holds
h . (k + 1) = subdivision (P,K1)
proof
let k be Nat; ::_thesis: for K1 being SimplicialComplexStr of X st h . k = K1 holds
h . (k + 1) = subdivision (P,K1)
let KK be SimplicialComplexStr of X; ::_thesis: ( h . k = KK implies h . (k + 1) = subdivision (P,KK) )
assume A26: h . k = KK ; ::_thesis: h . (k + 1) = subdivision (P,KK)
 S2[k + 1] by A16;
then consider K1 being SimplicialComplexStr of X such that
A27: the topology of K1 = g . (k + 1) and
A28: [#] K1 = [#] KX ;
reconsider TOP1 = the topology of K1 as Subset-Family of KX by A28;
A29: k in NAT by ORDINAL1:def_12;
 S2[k] by A16;
then consider K2 being SimplicialComplexStr of X such that
A30: the topology of K2 = g . k and
A31: [#] K2 = [#] KX ;
reconsider TOP2 = the topology of K2 as Subset-Family of KX by A31;
A32: [#] (subdivision (P,KK)) = [#] KK by Def20;
percases ( k = 0 or k > 0 ) ;
supposeA33: k = 0 ; ::_thesis: h . (k + 1) = subdivision (P,KK)
then  TOP1 = the topology of (subdivision (P,KK)) by A8, A10, A24, A26, A27;
hence  h . (k + 1) = subdivision (P,KK) by A22, A24, A26, A27, A32, A33; ::_thesis: verum
end;
suppose k > 0 ; ::_thesis: h . (k + 1) = subdivision (P,KK)
then A34: KK = TopStruct(# the carrier of KX,TOP2 #) by A22, A26, A29, A30;
then  [#] KK = [#] KX ;
then  g . (k + 1) = the topology of (subdivision (P,KK)) by A16, A30, A34;
hence  h . (k + 1) = subdivision (P,KK) by A22, A32, A34; ::_thesis: verum
end;
end;
end;
percases ( n = 0 or n > 0 ) ;
supposeA35: n = 0 ; ::_thesis: ex b1 being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
take  KX ; ::_thesis: ex F being Function st
( F . 0 = KX & F . n = KX & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
thus  ex F being Function st
( F . 0 = KX & F . n = KX & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) by A22, A24, A25, A35; ::_thesis: verum
end;
supposeA36: n > 0 ; ::_thesis: ex b1 being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
consider K1 being SimplicialComplexStr of X such that
A37: the topology of K1 = g . n and
A38: [#] K1 = [#] KX and
A39: ( n > 0 implies K1 is strict ) by A16;
reconsider K1 = K1 as strict SimplicialComplexStr of X by A36, A39;
take  K1 ; ::_thesis: ex F being Function st
( F . 0 = KX & F . n = K1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
take  h ; ::_thesis: ( h . 0 = KX & h . n = K1 & dom h = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = h . k holds
h . (k + 1) = subdivision (P,KX1) ) )
thus  h . 0 = KX by A22, A23; ::_thesis: ( h . n = K1 & dom h = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = h . k holds
h . (k + 1) = subdivision (P,KX1) ) )
 n in NAT by ORDINAL1:def_12;
hence  ( h . n = K1 & dom h = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = h . k holds
h . (k + 1) = subdivision (P,KX1) ) ) by A22, A25, A36, A37, A38; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being SimplicialComplexStr of X st ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) & ex F being Function st
( F . 0 = KX & F . n = b2 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) holds
b1 = b2
proof
let P1, P2 be SimplicialComplexStr of X; ::_thesis: ( ex F being Function st
( F . 0 = KX & F . n = P1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) & ex F being Function st
( F . 0 = KX & F . n = P2 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) implies P1 = P2 )
given F1 being Function such that A40: F1 . 0 = KX and
A41: F1 . n = P1 and
 dom F1 = NAT and
A42: for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F1 . k holds
F1 . (k + 1) = subdivision (P,KX1) ; ::_thesis: ( for F being Function holds
( not F . 0 = KX or not F . n = P2 or not dom F = NAT or ex k being Nat ex KX1 being SimplicialComplexStr of X st
( KX1 = F . k & not F . (k + 1) = subdivision (P,KX1) ) ) or P1 = P2 )
given F2 being Function such that A43: F2 . 0 = KX and
A44: F2 . n = P2 and
 dom F2 = NAT and
A45: for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F2 . k holds
F2 . (k + 1) = subdivision (P,KX1) ; ::_thesis: P1 = P2
defpred S1[ Nat] means ( F1 . $1 = F2 . $1 & ex KX1 being SimplicialComplexStr of X st KX1 = F1 . $1 );
A46: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A47: S1[k] ; ::_thesis: S1[k + 1]
consider KX1 being SimplicialComplexStr of X such that
A48: KX1 = F1 . k by A47;
 F1 . (k + 1) = subdivision (P,KX1) by A42, A48;
hence  S1[k + 1] by A45, A47, A48; ::_thesis: verum
end;
A49: S1[ 0 ] by A40, A43;
 for k being Nat holds S1[k] from NAT_1:sch_2(A49, A46);
hence  P1 = P2 by A41, A44; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines subdivision SIMPLEX0:def_21_:_
 for X being set
for KX being SimplicialComplexStr of X
for P being Function
for n being Nat
for b5 being SimplicialComplexStr of X holds
( b5 = subdivision (n,P,KX) iff ex F being Function st
( F . 0 = KX & F . n = b5 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) );

theorem Th61: :: SIMPLEX0:61
for X being set
for KX being SimplicialComplexStr of X
for P being Function holds subdivision (0,P,KX) = KX
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function holds subdivision (0,P,KX) = KX
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function holds subdivision (0,P,KX) = KX
let P be Function; ::_thesis: subdivision (0,P,KX) = KX
 ex F being Function st
( F . 0 = KX & F . 0 = subdivision (0,P,KX) & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) by Def21;
hence  subdivision (0,P,KX) = KX ; ::_thesis: verum
end;

theorem Th62: :: SIMPLEX0:62
for X being set
for KX being SimplicialComplexStr of X
for P being Function holds subdivision (1,P,KX) = subdivision (P,KX)
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function holds subdivision (1,P,KX) = subdivision (P,KX)
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function holds subdivision (1,P,KX) = subdivision (P,KX)
let P be Function; ::_thesis: subdivision (1,P,KX) = subdivision (P,KX)
consider F being Function such that
A1: F . 0 = KX and
A2: F . 1 = subdivision (1,P,KX) and
 dom F = NAT and
A3: for k being Nat
for KX1 being 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  subdivision (1,P,KX) = subdivision (P,KX) by A2; ::_thesis: verum
end;

theorem Th63: :: SIMPLEX0:63
for X being set
for KX being SimplicialComplexStr of X
for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
proof
let X be set ; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
let P be Function; ::_thesis: for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
let n, k be Element of NAT ; ::_thesis: subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
consider Fn being 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 being Nat
for KX1 being SimplicialComplexStr of X st KX1 = Fn . m holds
Fn . (m + 1) = subdivision (P,KX1) by Def21;
consider Fnm being 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 being Nat
for KX1 being SimplicialComplexStr of X st KX1 = Fnm . m holds
Fnm . (m + 1) = subdivision (P,KX1) by Def21;
defpred S1[ Nat] means ( $1 <= n implies ( Fn . $1 = Fnm . ($1 + k) & ex SX being SimplicialComplexStr of X st Fn . $1 = SX ) );
A7: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A8: S1[m] ; ::_thesis: S1[m + 1]
assume A9: m + 1 <= n ; ::_thesis: ( Fn . (m + 1) = Fnm . ((m + 1) + k) & ex SX being SimplicialComplexStr of X st Fn . (m + 1) = SX )
then consider SX being 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  ( Fn . (m + 1) = Fnm . ((m + 1) + k) & ex SX being SimplicialComplexStr of X st Fn . (m + 1) = SX ) by A3, A10; ::_thesis: verum
end;
consider Fm being Function such that
A11: Fm . 0 = KX and
A12: Fm . k = subdivision (k,P,KX) and
 dom Fm = NAT and
A13: for m being Nat
for KX1 being SimplicialComplexStr of X st KX1 = Fm . m holds
Fm . (m + 1) = subdivision (P,KX1) by Def21;
defpred S2[ Nat] means ( $1 <= k implies ( Fm . $1 = Fnm . $1 & ex SX being SimplicialComplexStr of X st Fm . $1 = SX ) );
A14: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A15: S2[m] ; ::_thesis: S2[m + 1]
assume A16: m + 1 <= k ; ::_thesis: ( Fm . (m + 1) = Fnm . (m + 1) & ex SX being SimplicialComplexStr of X st Fm . (m + 1) = SX )
then consider SX being 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  ( Fm . (m + 1) = Fnm . (m + 1) & ex SX being SimplicialComplexStr of X st Fm . (m + 1) = SX ) by A13, A17; ::_thesis: verum
end;
A18: S2[ 0 ] by A4, A11;
 for k being Nat holds S2[k] from NAT_1:sch_2(A18, A14);
then A19: S1[ 0 ] by A1, A12;
 for k being Nat holds S1[k] from NAT_1:sch_2(A19, A7);
hence  subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX))) by A2, A5; ::_thesis: verum
end;

theorem :: SIMPLEX0:64
for X being set
for n being Nat
for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
proof
let X be set ; ::_thesis: for n being Nat
for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
let n be Nat; ::_thesis: for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
let KX be SimplicialComplexStr of X; ::_thesis: for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
let P be Function; ::_thesis: [#] (subdivision (n,P,KX)) = [#] KX
defpred S1[ Nat] means  [#] (subdivision ($1,P,KX)) = [#] KX;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
 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 ; ::_thesis: S1[n + 1]
hence  S1[n + 1] by A2, Def20; ::_thesis: verum
end;
A3: S1[ 0 ] by Th61;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence  [#] (subdivision (n,P,KX)) = [#] KX ; ::_thesis: verum
end;

theorem :: SIMPLEX0:65
for X being set
for n being Nat
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
proof
let X be set ; ::_thesis: for n being Nat
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let n be Nat; ::_thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let KX be SimplicialComplexStr of X; ::_thesis: for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let SX be SubSimplicialComplex of KX; ::_thesis: for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let P be Function; ::_thesis: subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
defpred S1[ Nat] means  subdivision ($1,P,SX) is SubSimplicialComplex of subdivision ($1,P,KX);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
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  S1[n + 1] by A3, Th58; ::_thesis: verum
end;
 subdivision (0,P,SX) = SX by Th61;
then A4: S1[ 0 ] by Th61;
 for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence  subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX) ; ::_thesis: verum
end;