:: TRIANG_1 semantic presentation

begin


registration
let X be non empty set ;
let R be Order of X;
cluster RelStr(# X,R #) ->  non empty ;
coherence
 not RelStr(# X,R #) is empty ;
end;

theorem :: TRIANG_1:1
for A being set holds {} |_2 A = {} ;

theorem :: TRIANG_1:2
for F being non empty Poset
for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) holds
ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )
proof
let F be non empty Poset; ::_thesis: for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) holds
ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )
defpred S1[ set ] means ( $1 <> {} implies ex m being Element of F st
( m in $1 & ( for C being Element of F st C in $1 holds
m <= C ) ) );
let A be Subset of F; ::_thesis: ( A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) implies ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) ) )
assume that
A1: A is finite and
A2: A <> {} and
A3: for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ; ::_thesis: ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )
A4: now__::_thesis:_for_x_being_Element_of_F
for_B_being_Subset_of_F_st_x_in_A_&_B_c=_A_&_S1[B]_holds_
S1[B_\/_{x}]
let x be Element of F; ::_thesis: for B being Subset of F st x in A & B c= A & S1[B] holds
S1[B \/ {x}]
let B be Subset of F; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A5: x in A and
A6: B c= A and
A7: S1[B] ; ::_thesis: S1[B \/ {x}]
reconsider x9 = x as Element of F ;
now__::_thesis:_(_B_\/_{x}_<>_{}_implies_ex_m_being_Element_of_F_st_
(_m_in_B_\/_{x}_&_(_for_C_being_Element_of_F_st_C_in_B_\/_{x}_holds_
m_<=_C_)_)_)
percases ( for y being Element of F holds
( not y in B or not y <= x9 ) or ex y being Element of F st
( y in B & y <= x9 ) ) ;
supposeA8: for y being Element of F holds
( not y in B or not y <= x9 ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) ) )
assume  B \/ {x} <> {} ; ::_thesis: ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )
take m = x9; ::_thesis: ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )
 x in {x} by TARSKI:def_1;
hence  m in B \/ {x} by XBOOLE_0:def_3; ::_thesis: for C being Element of F st C in B \/ {x} holds
m <= C
let C be Element of F; ::_thesis: ( C in B \/ {x} implies m <= C )
assume  C in B \/ {x} ; ::_thesis: m <= C
then A9: ( C in B or C in {x} ) by XBOOLE_0:def_3;
then  ( not C <= x9 or C = x ) by A8, TARSKI:def_1;
hence  m <= C by A3, A5, A6, A9, TARSKI:def_1; ::_thesis: verum
end;
supposeA10: ex y being Element of F st
( y in B & y <= x9 ) ; ::_thesis: ( B \/ {x} <> {} implies ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) ) )
assume  B \/ {x} <> {} ; ::_thesis: ex m being Element of F st
( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )
consider y being Element of F such that
A11: y in B and
A12: y <= x9 by A10;
consider m being Element of F such that
A13: m in B and
A14: for C being Element of F st C in B holds
m <= C by A7, A11;
take m = m; ::_thesis: ( m in B \/ {x} & ( for C being Element of F st C in B \/ {x} holds
m <= C ) )
thus  m in B \/ {x} by A13, XBOOLE_0:def_3; ::_thesis: for C being Element of F st C in B \/ {x} holds
m <= C
let C be Element of F; ::_thesis: ( C in B \/ {x} implies m <= C )
assume  C in B \/ {x} ; ::_thesis: m <= C
then A15: ( C in B or C in {x} ) by XBOOLE_0:def_3;
 m <= y by A11, A14;
then  m <= x9 by A12, ORDERS_2:3;
hence  m <= C by A14, A15, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  S1[B \/ {x}] ; ::_thesis: verum
end;
A16: S1[ {} the carrier of F] ;
 S1[A] from PRE_POLY:sch_2(A1, A16, A4);
hence  ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) ) by A2; ::_thesis: verum
end;

registration
let P be non empty Poset;
let A be non empty finite Subset of P;
let x be Element of P;
cluster InitSegm (A,x) ->  finite ;
coherence
 InitSegm (A,x) is finite ;
end;

begin

definition
let C be non empty Poset;
func symplexes C ->  Subset of (Fin the carrier of C) equals :: TRIANG_1:def 1
 {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ;
coherence
  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  is Subset of (Fin the carrier of C)
proof
set S =  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ;
  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  c= Fin the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  or x in Fin the carrier of C )
assume  x in  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ; ::_thesis: x in Fin the carrier of C
then  ex a being Element of Fin the carrier of C st
( x = a & the InternalRel of C linearly_orders a ) ;
hence  x in Fin the carrier of C ; ::_thesis: verum
end;
hence   {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  is Subset of (Fin the carrier of C) ; ::_thesis: verum
end;
end;

:: deftheorem  defines symplexes TRIANG_1:def_1_:_
 for C being non empty Poset holds symplexes C =  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ;

registration
let C be non empty Poset;
cluster symplexes C ->  with_non-empty_element ;
coherence
 not symplexes C is empty-membered
proof
set x = the Element of C;
reconsider a = { the Element of C} as Element of Fin the carrier of C by FINSUB_1:def_5;
A1: the InternalRel of C is_connected_in a
proof
let k, l be set ; :: according to RELAT_2:def_6 ::_thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
assume that
A2: k in a and
A3: l in a and
A4: k <> l ; ::_thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
 k = the Element of C by A2, TARSKI:def_1;
hence  ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
A5: field the InternalRel of C = the carrier of C by ORDERS_1:12;
then  the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def_12;
then A6: the InternalRel of C is_antisymmetric_in a by ORDERS_1:9;
 the InternalRel of C is_transitive_in the carrier of C by A5, RELAT_2:def_16;
then A7: the InternalRel of C is_transitive_in a by ORDERS_1:10;
 the InternalRel of C is_reflexive_in the carrier of C by A5, RELAT_2:def_9;
then  the InternalRel of C is_reflexive_in a by ORDERS_1:8;
then  the InternalRel of C linearly_orders a by A6, A7, A1, ORDERS_1:def_8;
then  a in  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ;
hence  not symplexes C is empty-membered by SETFAM_1:def_10; ::_thesis: verum
end;
end;

theorem Th3: :: TRIANG_1:3
for C being non empty Poset
for x being Element of C holds {x} in symplexes C
proof
let C be non empty Poset; ::_thesis: for x being Element of C holds {x} in symplexes C
let x be Element of C; ::_thesis: {x} in symplexes C
reconsider a = {x} as Element of Fin the carrier of C by FINSUB_1:def_5;
A1: the InternalRel of C is_connected_in a
proof
let k, l be set ; :: according to RELAT_2:def_6 ::_thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
assume that
A2: k in a and
A3: l in a and
A4: k <> l ; ::_thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
 k = x by A2, TARSKI:def_1;
hence  ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
A5: field the InternalRel of C = the carrier of C by ORDERS_1:12;
then  the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def_12;
then A6: the InternalRel of C is_antisymmetric_in a by ORDERS_1:9;
 the InternalRel of C is_transitive_in the carrier of C by A5, RELAT_2:def_16;
then A7: the InternalRel of C is_transitive_in a by ORDERS_1:10;
 the InternalRel of C is_reflexive_in the carrier of C by A5, RELAT_2:def_9;
then  the InternalRel of C is_reflexive_in a by ORDERS_1:8;
then  the InternalRel of C linearly_orders a by A6, A7, A1, ORDERS_1:def_8;
hence  {x} in symplexes C ; ::_thesis: verum
end;

theorem :: TRIANG_1:4
for C being non empty Poset holds {} in symplexes C
proof
let C be non empty Poset; ::_thesis: {} in symplexes C
A1: {} is Subset of C by SUBSET_1:1;
then reconsider a = {} as Element of Fin the carrier of C by FINSUB_1:def_5;
A2: field the InternalRel of C = the carrier of C by ORDERS_1:12;
then  the InternalRel of C is_antisymmetric_in the carrier of C by RELAT_2:def_12;
then A3: the InternalRel of C is_antisymmetric_in a by A1, ORDERS_1:9;
A4: the InternalRel of C is_connected_in a
proof
let k, l be set ; :: according to RELAT_2:def_6 ::_thesis: ( not k in a or not l in a or k = l or [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
assume that
A5: k in a and
 l in a and
 k <> l ; ::_thesis: ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C )
thus  ( [k,l] in the InternalRel of C or [l,k] in the InternalRel of C ) by A5; ::_thesis: verum
end;
 the InternalRel of C is_transitive_in the carrier of C by A2, RELAT_2:def_16;
then A6: the InternalRel of C is_transitive_in a by A1, ORDERS_1:10;
 the InternalRel of C is_reflexive_in the carrier of C by A2, RELAT_2:def_9;
then  the InternalRel of C is_reflexive_in a by A1, ORDERS_1:8;
then  the InternalRel of C linearly_orders a by A3, A6, A4, ORDERS_1:def_8;
hence  {} in symplexes C ; ::_thesis: verum
end;

theorem Th5: :: TRIANG_1:5
for C being non empty Poset
for x, s being set st x c= s & s in symplexes C holds
x in symplexes C
proof
let C be non empty Poset; ::_thesis: for x, s being set st x c= s & s in symplexes C holds
x in symplexes C
let x, s be set ; ::_thesis: ( x c= s & s in symplexes C implies x in symplexes C )
assume that
A1: x c= s and
A2: s in symplexes C ; ::_thesis: x in symplexes C
consider s1 being Element of Fin the carrier of C such that
A3: s1 = s and
A4: the InternalRel of C linearly_orders s1 by A2;
 s1 c= the carrier of C by FINSUB_1:def_5;
then  x c= the carrier of C by A1, A3, XBOOLE_1:1;
then reconsider x1 = x as Element of Fin the carrier of C by A1, A2, FINSUB_1:def_5;
 the InternalRel of C linearly_orders x by A1, A3, A4, ORDERS_1:38;
then  x1 in  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ;
hence  x in symplexes C ; ::_thesis: verum
end;

theorem Th6: :: TRIANG_1:6
for n being Element of NAT
for C being non empty Poset
for A being non empty Element of symplexes C st card A = n holds
dom (SgmX ( the InternalRel of C,A)) = Seg n
proof
let n be Element of NAT ; ::_thesis: for C being non empty Poset
for A being non empty Element of symplexes C st card A = n holds
dom (SgmX ( the InternalRel of C,A)) = Seg n
let C be non empty Poset; ::_thesis: for A being non empty Element of symplexes C st card A = n holds
dom (SgmX ( the InternalRel of C,A)) = Seg n
let A be non empty Element of symplexes C; ::_thesis: ( card A = n implies dom (SgmX ( the InternalRel of C,A)) = Seg n )
set f = SgmX ( the InternalRel of C,A);
 A in  {  A1 where A1 is Element of Fin the carrier of C : the InternalRel of C linearly_orders A1  }  ;
then A1: ex A1 being Element of Fin the carrier of C st
( A1 = A & the InternalRel of C linearly_orders A1 ) ;
assume  card A = n ; ::_thesis: dom (SgmX ( the InternalRel of C,A)) = Seg n
then  len (SgmX ( the InternalRel of C,A)) = n by A1, PRE_POLY:11;
hence  dom (SgmX ( the InternalRel of C,A)) = Seg n by FINSEQ_1:def_3; ::_thesis: verum
end;

registration
let C be non empty Poset;
cluster non empty finite for Element of symplexes C;
existence
 not for b1 being Element of symplexes C holds b1 is empty
proof
set x = the Element of C;
 { the Element of C} in symplexes C by Th3;
hence  not for b1 being Element of symplexes C holds b1 is empty ; ::_thesis: verum
end;
end;

begin

definition
mode SetSequence is ManySortedSet of NAT ;
end;

definition
let IT be SetSequence;
attrIT is lower_non-empty  means :Def2: :: TRIANG_1:def 2
 for n being Nat st not IT . n is empty holds
for m being Nat st m < n holds
not IT . m is empty ;
end;

:: deftheorem Def2 defines lower_non-empty TRIANG_1:def_2_:_
 for IT being SetSequence holds
( IT is lower_non-empty iff for n being Nat st not IT . n is empty holds
for m being Nat st m < n holds
not IT . m is empty );

registration
cluster Relation-like NAT -defined Function-like total lower_non-empty for set ;
existence
 ex b1 being SetSequence st b1 is lower_non-empty
proof
set f = NAT --> 1;
reconsider f = NAT --> 1 as ManySortedSet of NAT ;
take  f ; ::_thesis: f is lower_non-empty
 for n being Nat st not f . n is empty holds
for m being Nat st m < n holds
not f . m is empty
proof
let n be Nat; ::_thesis: ( not f . n is empty implies for m being Nat st m < n holds
not f . m is empty )
assume  not f . n is empty ; ::_thesis: for m being Nat st m < n holds
not f . m is empty
let m be Nat; ::_thesis: ( m < n implies not f . m is empty )
assume  m < n ; ::_thesis: not f . m is empty
 m in NAT by ORDINAL1:def_12;
hence  not f . m is empty by FUNCOP_1:7; ::_thesis: verum
end;
hence  f is lower_non-empty by Def2; ::_thesis: verum
end;
end;

definition
let X be SetSequence;
func FuncsSeq X ->  SetSequence means :Def3: :: TRIANG_1:def 3
 for n being Nat holds it . n = Funcs ((X . (n + 1)),(X . n));
existence
 ex b1 being SetSequence st
for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n))
proof
deffunc H1( Element of NAT ) ->  set = Funcs ((X . ($1 + 1)),(X . $1));
consider f being ManySortedSet of NAT  such that
A1: for n being Element of NAT holds f . n = H1(n) from PBOOLE:sch_5();
reconsider f = f as SetSequence ;
take  f ; ::_thesis: for n being Nat holds f . n = Funcs ((X . (n + 1)),(X . n))
let n be Nat; ::_thesis: f . n = Funcs ((X . (n + 1)),(X . n))
 n in NAT by ORDINAL1:def_12;
hence  f . n = Funcs ((X . (n + 1)),(X . n)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence st ( for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) ) holds
b1 = b2
proof
let a, b be SetSequence; ::_thesis: ( ( for n being Nat holds a . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b . n = Funcs ((X . (n + 1)),(X . n)) ) implies a = b )
assume that
A2: for n being Nat holds a . n = Funcs ((X . (n + 1)),(X . n)) and
A3: for n being Nat holds b . n = Funcs ((X . (n + 1)),(X . n)) ; ::_thesis: a = b
let n be Element of NAT ; :: according to PBOOLE:def_21 ::_thesis: a . n = b . n
 a . n = Funcs ((X . (n + 1)),(X . n)) by A2;
hence  a . n c= b . n by A3; :: according to XBOOLE_0:def_10 ::_thesis: b . n c= a . n
 a . n = Funcs ((X . (n + 1)),(X . n)) by A2;
hence  b . n c= a . n by A3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines FuncsSeq TRIANG_1:def_3_:_
 for X, b2 being SetSequence holds
( b2 = FuncsSeq X iff for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) );

registration
let X be lower_non-empty SetSequence;
let n be Nat;
cluster(FuncsSeq X) . n ->  non empty ;
coherence
 not (FuncsSeq X) . n is empty
proof
 n < n + 1 by NAT_1:13;
then A1: ( X . (n + 1) = {} or X . n <> {} ) by Def2;
 (FuncsSeq X) . n = Funcs ((X . (n + 1)),(X . n)) by Def3;
hence  not (FuncsSeq X) . n is empty by A1, FUNCT_2:8; ::_thesis: verum
end;
end;

definition
let n be Nat;
let f be Element of Funcs ((Seg n),(Seg (n + 1)));
func @ f ->  FinSequence of REAL  equals :: TRIANG_1:def 4
f;
coherence
 f is FinSequence of REAL
proof
consider x being Function such that
A1: x = f and
 dom x = Seg n and
 rng x c= Seg (n + 1) by FUNCT_2:def_2;
reconsider x = x as FinSequence of Seg (n + 1) by A1, FINSEQ_2:25;
 Seg (n + 1) c= REAL by XBOOLE_1:1;
then  x is FinSequence of REAL by FINSEQ_2:24;
hence  f is FinSequence of REAL by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines @ TRIANG_1:def_4_:_
 for n being Nat
for f being Element of Funcs ((Seg n),(Seg (n + 1))) holds @ f = f;

definition
func NatEmbSeq  ->  SetSequence means :Def5: :: TRIANG_1:def 5
 for n being Nat holds it . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ;
existence
 ex b1 being SetSequence st
for n being Nat holds b1 . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }
proof
deffunc H1( Element of NAT ) ->  set =  {  f where f is Element of Funcs ((Seg $1),(Seg ($1 + 1))) : @ f is increasing  }  ;
consider F being ManySortedSet of NAT  such that
A1: for n being Element of NAT holds F . n = H1(n) from PBOOLE:sch_5();
reconsider F = F as SetSequence ;
take  F ; ::_thesis: for n being Nat holds F . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }
let n be Nat; ::_thesis: F . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }
 n in NAT by ORDINAL1:def_12;
hence  F . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence st ( for n being Nat holds b1 . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ) & ( for n being Nat holds b2 . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ) holds
b1 = b2
proof
let a, b be SetSequence; ::_thesis: ( ( for n being Nat holds a . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ) & ( for n being Nat holds b . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ) implies a = b )
assume that
A2: for n being Nat holds a . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  and
A3: for n being Nat holds b . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ; ::_thesis: a = b
let n be Element of NAT ; :: according to PBOOLE:def_21 ::_thesis: a . n = b . n
 a . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  by A2;
hence  a . n c= b . n by A3; :: according to XBOOLE_0:def_10 ::_thesis: b . n c= a . n
 a . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  by A2;
hence  b . n c= a . n by A3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines NatEmbSeq TRIANG_1:def_5_:_
 for b1 being SetSequence holds
( b1 = NatEmbSeq iff for n being Nat holds b1 . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  );

registration
let n be Nat;
clusterNatEmbSeq . n ->  non empty ;
coherence
 not NatEmbSeq . n is empty
proof
 n <= n + 1 by NAT_1:11;
then A1: Seg n c= Seg (n + 1) by FINSEQ_1:5;
A2: rng (id (Seg n)) = Seg n ;
 dom (id (Seg n)) = Seg n ;
then reconsider n1 = idseq n as Element of Funcs ((Seg n),(Seg (n + 1))) by A1, A2, FUNCT_2:def_2;
 @ n1 is increasing ;
then  n1 in  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  ;
hence  not NatEmbSeq . n is empty by Def5; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster  ->  Relation-like Function-like for Element of NatEmbSeq . n;
coherence
 for b1 being Element of NatEmbSeq . n holds
( b1 is Function-like & b1 is Relation-like )
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
let x be Element of NatEmbSeq . n; ::_thesis: ( x is Function-like & x is Relation-like )
A1: x in NatEmbSeq . n9 ;
 NatEmbSeq . n =  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  by Def5;
then  ex f being Element of Funcs ((Seg n),(Seg (n + 1))) st
( x = f & @ f is increasing ) by A1;
hence  ( x is Function-like & x is Relation-like ) ; ::_thesis: verum
end;
end;

definition
let X be SetSequence;
mode triangulation of X is ManySortedFunction of NatEmbSeq , FuncsSeq X;
end;

definition
attrc1 is strict ;
struct TriangStr  -> ;
aggrTriangStr(# SkeletonSeq, FacesAssign #) ->  TriangStr ;
sel SkeletonSeq c1 ->  SetSequence;
sel FacesAssign c1 ->  ManySortedFunction of NatEmbSeq , FuncsSeq the SkeletonSeq of c1;
end;

definition
let T be TriangStr ;
attrT is lower_non-empty  means :Def6: :: TRIANG_1:def 6
 the SkeletonSeq of T is lower_non-empty ;
end;

:: deftheorem Def6 defines lower_non-empty TRIANG_1:def_6_:_
 for T being TriangStr holds
( T is lower_non-empty iff the SkeletonSeq of T is lower_non-empty );

registration
cluster strict lower_non-empty for TriangStr ;
existence
 ex b1 being TriangStr st
( b1 is lower_non-empty & b1 is strict )
proof
set Sk = NAT --> {};
reconsider Sk = NAT --> {} as ManySortedSet of NAT ;
set A = the ManySortedFunction of NatEmbSeq , FuncsSeq Sk;
take  TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) ; ::_thesis: ( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict )
 for n being Nat st not Sk . n is empty holds
for m being Nat st m < n holds
not Sk . m is empty
proof
let n be Nat; ::_thesis: ( not Sk . n is empty implies for m being Nat st m < n holds
not Sk . m is empty )
assume A1: not Sk . n is empty ; ::_thesis: for m being Nat st m < n holds
not Sk . m is empty
 n in NAT by ORDINAL1:def_12;
hence  for m being Nat st m < n holds
not Sk . m is empty by A1, FUNCOP_1:7; ::_thesis: verum
end;
then  Sk is lower_non-empty by Def2;
hence  ( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict ) by Def6; ::_thesis: verum
end;
end;

registration
let T be lower_non-empty TriangStr ;
cluster the SkeletonSeq of T ->  lower_non-empty ;
coherence
 the SkeletonSeq of T is lower_non-empty by Def6;
end;

registration
let S be lower_non-empty SetSequence;
let F be ManySortedFunction of NatEmbSeq , FuncsSeq S;
cluster TriangStr(# S,F #) ->  lower_non-empty ;
coherence
 TriangStr(# S,F #) is lower_non-empty by Def6;
end;

begin

definition
let T be TriangStr ;
let n be Nat;
mode Symplex of T,n is Element of the SkeletonSeq of T . n;
end;

definition
let n be Nat;
mode Face of n is Element of NatEmbSeq . n;
end;

definition
let T be lower_non-empty TriangStr ;
let n be Nat;
let x be Symplex of T,(n + 1);
let f be Face of n;
assume A1: the SkeletonSeq of T . (n + 1) <> {} ;
func face (x,f) ->  Symplex of T,n means :Def7: :: TRIANG_1:def 7
 for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
it = G . x;
existence
 ex b1 being Symplex of T,n st
for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b1 = G . x
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
reconsider F = the FacesAssign of T . n9 as Function of (NatEmbSeq . n9),((FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def_15;
 F . f in (FuncsSeq the SkeletonSeq of T) . n9 by FUNCT_2:5;
then  F . f in Funcs (( the SkeletonSeq of T . (n + 1)),( the SkeletonSeq of T . n)) by Def3;
then consider G being Function such that
A2: G = F . f and
A3: dom G = the SkeletonSeq of T . (n + 1) and
A4: rng G c= the SkeletonSeq of T . n by FUNCT_2:def_2;
 G . x in rng G by A1, A3, FUNCT_1:def_3;
then reconsider S = G . x as Symplex of T,n by A4;
take  S ; ::_thesis: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S = G . x
let F1, G1 be Function; ::_thesis: ( F1 = the FacesAssign of T . n & G1 = F1 . f implies S = G1 . x )
assume that
A5: F1 = the FacesAssign of T . n and
A6: G1 = F1 . f ; ::_thesis: S = G1 . x
thus  S = G1 . x by A2, A5, A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b2 = G . x ) holds
b1 = b2
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
let S1, S2 be Symplex of T,n; ::_thesis: ( ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S2 = G . x ) implies S1 = S2 )
assume that
A7: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S1 = G . x and
A8: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S2 = G . x ; ::_thesis: S1 = S2
reconsider F = the FacesAssign of T . n9 as Function of (NatEmbSeq . n9),((FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def_15;
 F . f in (FuncsSeq the SkeletonSeq of T) . n9 by FUNCT_2:5;
then  F . f in Funcs (( the SkeletonSeq of T . (n + 1)),( the SkeletonSeq of T . n)) by Def3;
then consider G being Function such that
A9: G = F . f and
 dom G = the SkeletonSeq of T . (n + 1) and
 rng G c= the SkeletonSeq of T . n by FUNCT_2:def_2;
 S1 = G . x by A7, A9;
hence  S1 = S2 by A8, A9; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines face TRIANG_1:def_7_:_
 for T being lower_non-empty TriangStr
for n being Nat
for x being Symplex of T,(n + 1)
for f being Face of n st the SkeletonSeq of T . (n + 1) <> {} holds
for b5 being Symplex of T,n holds
( b5 = face (x,f) iff for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b5 = G . x );

definition
let C be non empty Poset;
func Triang C ->  strict lower_non-empty TriangStr  means :: TRIANG_1:def 8
( the SkeletonSeq of it . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of it . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of it . (n + 1) st s in the SkeletonSeq of it . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) );
existence
 ex b1 being strict lower_non-empty TriangStr st
( the SkeletonSeq of b1 . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b1 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) )
proof
deffunc H1( Element of NAT ) ->  set = IFEQ ($1,0,{{}}, {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = $1  }  );
consider Sk being SetSequence such that
A1: for n being Element of NAT holds Sk . n = H1(n) from PBOOLE:sch_5();
A2: now__::_thesis:_for_n_being_Nat_st_n_<>_0_holds_
Sk_._n_=__{__(SgmX_(_the_InternalRel_of_C,s))_where_s_is_non_empty_Element_of_symplexes_C_:_card_s_=_n__}_
let n be Nat; ::_thesis: ( n <> 0 implies Sk . n =  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }  )
assume A3: n <> 0 ; ::_thesis: Sk . n =  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }
 n in NAT by ORDINAL1:def_12;
hence Sk . n = IFEQ (n,0,{{}}, {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }  ) by A1
.=  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }  by A3, FUNCOP_1:def_8 ;
::_thesis: verum
end;
A4: Sk . 0 = IFEQ (0,0,{{}}, {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = 0  }  ) by A1
.= {{}} by FUNCOP_1:def_8 ;
 Sk is lower_non-empty
proof
defpred S1[ Nat] means  not Sk . $1 is empty ;
let n be Nat; :: according to TRIANG_1:def_2 ::_thesis: ( not Sk . n is empty implies for m being Nat st m < n holds
not Sk . m is empty )
A5: for m being Element of NAT st m < n & S1[m + 1] holds
S1[m]
proof
let m be Element of NAT ; ::_thesis: ( m < n & S1[m + 1] implies S1[m] )
assume that
 m < n and
A6: not Sk . (m + 1) is empty ; ::_thesis: S1[m]
consider g being set  such that
A7: g in Sk . (m + 1) by A6, XBOOLE_0:def_1;
 Sk . (m + 1) =  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = m + 1  }  by A2;
then consider s being non empty Element of symplexes C such that
 g = SgmX ( the InternalRel of C,s) and
A8: card s = m + 1 by A7;
set x = the Element of s;
reconsider sx = s \ { the Element of s} as finite set ;
 sx \/ { the Element of s} = s \/ { the Element of s} by XBOOLE_1:39;
then A9: sx \/ { the Element of s} = s by XBOOLE_1:12;
 not the Element of s in sx by ZFMISC_1:56;
then A10: m + 1 = (card sx) + 1 by A8, A9, CARD_2:41;
percases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; ::_thesis: S1[m]
hence  S1[m] by A4; ::_thesis: verum
end;
supposeA11: m <> 0 ; ::_thesis: S1[m]
then reconsider sx = sx as non empty Element of symplexes C by A10, Th5, XBOOLE_1:36;
 SgmX ( the InternalRel of C,sx) in  {  (SgmX ( the InternalRel of C,s1)) where s1 is non empty Element of symplexes C : card s1 = m  }  by A10;
hence  S1[m] by A2, A11; ::_thesis: verum
end;
end;
end;
assume A12: S1[n] ; ::_thesis: for m being Nat st m < n holds
not Sk . m is empty
A13: for m being Element of NAT st m <= n holds
S1[m] from PRE_POLY:sch_1(A12, A5);
let m be Nat; ::_thesis: ( m < n implies not Sk . m is empty )
assume A14: m < n ; ::_thesis: not Sk . m is empty
 m in NAT by ORDINAL1:def_12;
hence  not Sk . m is empty by A13, A14; ::_thesis: verum
end;
then reconsider Sk = Sk as lower_non-empty SetSequence ;
defpred S1[ set , set , set ] means  ex n being Nat ex y being Face of n st
( $2 = y & $3 = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = $1 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) );
A15: for i being set st i in NAT holds
for x being set st x in NatEmbSeq . i holds
ex y being set st
( y in (FuncsSeq Sk) . i & S1[y,x,i] )
proof
let i be set ; ::_thesis: ( i in NAT implies for x being set st x in NatEmbSeq . i holds
ex y being set st
( y in (FuncsSeq Sk) . i & S1[y,x,i] ) )
assume  i in NAT ; ::_thesis: for x being set st x in NatEmbSeq . i holds
ex y being set st
( y in (FuncsSeq Sk) . i & S1[y,x,i] )
then reconsider n = i as Element of NAT ;
let x be set ; ::_thesis: ( x in NatEmbSeq . i implies ex y being set st
( y in (FuncsSeq Sk) . i & S1[y,x,i] ) )
assume A16: x in NatEmbSeq . i ; ::_thesis: ex y being set st
( y in (FuncsSeq Sk) . i & S1[y,x,i] )
then reconsider y = x as Face of n ;
reconsider y1 = y as Function ;
 x in  {  f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing  }  by A16, Def5;
then A17: ex f being Element of Funcs ((Seg n),(Seg (n + 1))) st
( f = x & @ f is increasing ) ;
then consider y2 being Function such that
A18: y2 = y1 and
A19: dom y2 = Seg n and
A20: rng y2 c= Seg (n + 1) by FUNCT_2:def_2;
reconsider y2 = y2 as FinSequence by A19, FINSEQ_1:def_2;
A21: len y2 = n by A19, FINSEQ_1:def_3;
defpred S2[ set , set ] means  ex f being Function st
( f = $1 & $2 = f * y1 );
A22: for s being set st s in Sk . (n + 1) holds
ex u being set st S2[s,u]
proof
let s be set ; ::_thesis: ( s in Sk . (n + 1) implies ex u being set st S2[s,u] )
assume  s in Sk . (n + 1) ; ::_thesis: ex u being set st S2[s,u]
then  s in  {  (SgmX ( the InternalRel of C,s9)) where s9 is non empty Element of symplexes C : card s9 = n + 1  }  by A2;
then consider A being non empty Element of symplexes C such that
A23: SgmX ( the InternalRel of C,A) = s and
 card A = n + 1 ;
reconsider u = (SgmX ( the InternalRel of C,A)) * y as set ;
consider f being Function such that
A24: f = s by A23;
take  u ; ::_thesis: S2[s,u]
take  f ; ::_thesis: ( f = s & u = f * y1 )
thus  ( f = s & u = f * y1 ) by A23, A24; ::_thesis: verum
end;
consider g being Function such that
A25: dom g = Sk . (n + 1) and
A26: for s being set st s in Sk . (n + 1) holds
S2[s,g . s] from CLASSES1:sch_1(A22);
reconsider y2 = y2 as FinSequence of Seg (n + 1) by A20, FINSEQ_1:def_4;
reconsider g9 = g as set ;
take  g9 ; ::_thesis: ( g9 in (FuncsSeq Sk) . i & S1[g9,x,i] )
A27: y2 is one-to-one
proof
let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in dom y2 or not b in dom y2 or not y2 . a = y2 . b or a = b )
assume that
A28: a in dom y2 and
A29: b in dom y2 and
A30: y2 . a = y2 . b ; ::_thesis: a = b
reconsider a = a, b = b as Element of NAT by A28, A29;
now__::_thesis:_not_a_<>_b
assume A31: a <> b ; ::_thesis: contradiction
percases ( a < b or b < a ) by A31, XXREAL_0:1;
suppose a < b ; ::_thesis: contradiction
hence  contradiction by A17, A18, A28, A29, A30, SEQM_3:def_1; ::_thesis: verum
end;
suppose b < a ; ::_thesis: contradiction
hence  contradiction by A17, A18, A28, A29, A30, SEQM_3:def_1; ::_thesis: verum
end;
end;
end;
hence  a = b ; ::_thesis: verum
end;
 rng g c= Sk . n
proof
reconsider F = symplexes C as with_non-empty_element Subset of (Fin the carrier of C) ;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in Sk . n )
assume  z in rng g ; ::_thesis: z in Sk . n
then consider a being set  such that
A32: a in dom g and
A33: z = g . a by FUNCT_1:def_3;
consider f being Function such that
A34: f = a and
A35: g . a = f * y2 by A18, A25, A26, A32;
percases ( n = 0 or n <> 0 ) ;
supposeA36: n = 0 ; ::_thesis: z in Sk . n
then  Seg n = {} ;
then  dom (f * y1) = {} by A18, A19, RELAT_1:25, XBOOLE_1:3;
then  z = {} by A18, A33, A35;
hence  z in Sk . n by A4, A36, TARSKI:def_1; ::_thesis: verum
end;
supposeA37: n <> 0 ; ::_thesis: z in Sk . n
 f in  {  (SgmX ( the InternalRel of C,s1)) where s1 is non empty Element of symplexes C : card s1 = n + 1  }  by A2, A25, A32, A34;
then consider s1 being non empty Element of symplexes C such that
A38: SgmX ( the InternalRel of C,s1) = f and
A39: card s1 = n + 1 ;
 s1 in  {  A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A  }  ;
then A40: ex s19 being Element of Fin the carrier of C st
( s19 = s1 & the InternalRel of C linearly_orders s19 ) ;
then  rng f = s1 by A38, PRE_POLY:def_2;
then reconsider f = f as FinSequence of s1 by A38, FINSEQ_1:def_4;
reconsider f = f as FinSequence of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A41: f is one-to-one by A38, A40, PRE_POLY:10;
A42: dom f = Seg (n + 1) by A38, A39, Th6;
A43: f is Function of (dom f),s1 by FINSEQ_2:26;
then  f is Function of (Seg (n + 1)), the carrier of C by A42, FUNCT_2:7;
then reconsider z1 = z as FinSequence of RelStr(# the carrier of C, the InternalRel of C #) by A33, A35, FINSEQ_2:32;
reconsider f = f as Function of (Seg (n + 1)), the carrier of C by A42, A43, FUNCT_2:7;
A44: dom (f * y2) = Seg n by A19, A20, A42, RELAT_1:27;
 rng (f * y2) c= the carrier of C by FINSEQ_1:def_4;
then reconsider r = rng (f * y2) as Element of Fin the carrier of C by FINSUB_1:def_5;
 rng (f * y2) c= s1 by RELAT_1:def_19;
then reconsider s9 = r as non empty Element of F by A37, A44, Th5, RELAT_1:42;
 for n1, m1 being Nat st n1 in dom z1 & m1 in dom z1 & n1 < m1 holds
( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C )
proof
let n1, m1 be Nat; ::_thesis: ( n1 in dom z1 & m1 in dom z1 & n1 < m1 implies ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) )
assume that
A45: n1 in dom z1 and
A46: m1 in dom z1 and
A47: n1 < m1 ; ::_thesis: ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C )
 y2 . m1 in Seg (n + 1) by A19, A33, A35, A44, A46, FINSEQ_2:11;
then reconsider ym = y2 . m1 as Element of NAT ;
 y2 . n1 in Seg (n + 1) by A19, A33, A35, A44, A45, FINSEQ_2:11;
then reconsider yn = y2 . n1 as Element of NAT ;
A48: yn < ym by A17, A18, A19, A33, A35, A44, A45, A46, A47, SEQM_3:def_1;
A49: ym in rng y2 by A19, A33, A35, A44, A46, FUNCT_1:def_3;
then reconsider fm = f . ym as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2:11;
A50: fm = f /. ym by A20, A42, A49, PARTFUN1:def_6;
 z1 . m1 = fm by A33, A35, A46, FUNCT_1:12;
then reconsider zm = z1 . m1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A51: zm = z1 /. m1 by A46, PARTFUN1:def_6;
A52: z1 . m1 = f . (y2 . m1) by A33, A35, A46, FUNCT_1:12;
A53: z1 . n1 = f . (y2 . n1) by A33, A35, A45, FUNCT_1:12;
A54: yn in rng y2 by A19, A33, A35, A44, A45, FUNCT_1:def_3;
then reconsider fn = f . yn as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2:11;
 z1 . n1 = fn by A33, A35, A45, FUNCT_1:12;
then reconsider zn = z1 . n1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A55: zn = z1 /. n1 by A45, PARTFUN1:def_6;
 fn = f /. yn by A20, A42, A54, PARTFUN1:def_6;
hence  ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) by A20, A38, A40, A42, A53, A52, A48, A54, A49, A50, A55, A51, PRE_POLY:def_2; ::_thesis: verum
end;
then A56: z1 = SgmX ( the InternalRel of C,s9) by A33, A35, PRE_POLY:9;
 len (f * y2) = n by A20, A21, A42, FINSEQ_2:29;
then  card s9 = n by A27, A41, FINSEQ_4:62;
then  z in  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }  by A56;
hence  z in Sk . n by A2, A37; ::_thesis: verum
end;
end;
end;
then  g9 in Funcs ((Sk . (n + 1)),(Sk . n)) by A25, FUNCT_2:def_2;
hence  g9 in (FuncsSeq Sk) . i by Def3; ::_thesis: S1[g9,x,i]
reconsider y = x as Face of n by A16;
take  n ; ::_thesis: ex y being Face of n st
( x = y & i = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) )
take  y ; ::_thesis: ( x = y & i = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) )
thus  ( x = y & i = n ) ; ::_thesis: for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y
let s be Element of Sk . (n + 1); ::_thesis: ( s in Sk . (n + 1) implies for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y )
assume  s in Sk . (n + 1) ; ::_thesis: for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y
then A57: ex f being Function st
( f = s & g . s = f * y1 ) by A26;
let A be non empty Element of symplexes C; ::_thesis: ( SgmX ( the InternalRel of C,A) = s implies for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y )
assume A58: SgmX ( the InternalRel of C,A) = s ; ::_thesis: for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y
let g1 be Function; ::_thesis: ( g1 = g9 implies g1 . s = (SgmX ( the InternalRel of C,A)) * y )
assume  g1 = g9 ; ::_thesis: g1 . s = (SgmX ( the InternalRel of C,A)) * y
hence  g1 . s = (SgmX ( the InternalRel of C,A)) * y by A58, A57; ::_thesis: verum
end;
consider F being ManySortedFunction of NatEmbSeq , FuncsSeq Sk such that
A59: for i being set st i in NAT holds
ex f being Function of (NatEmbSeq . i),((FuncsSeq Sk) . i) st
( f = F . i & ( for x being set st x in NatEmbSeq . i holds
S1[f . x,x,i] ) ) from MSSUBFAM:sch_1(A15);
take  TriangStr(# Sk,F #) ; ::_thesis: ( the SkeletonSeq of TriangStr(# Sk,F #) . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of TriangStr(# Sk,F #) . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) )
thus  the SkeletonSeq of TriangStr(# Sk,F #) . 0 = {{}} by A4; ::_thesis: ( ( for n being Nat st n > 0 holds
the SkeletonSeq of TriangStr(# Sk,F #) . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) )
thus  for n being Nat st n > 0 holds
the SkeletonSeq of TriangStr(# Sk,F #) . n =  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }  by A2; ::_thesis: for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f
let n be Nat; ::_thesis: for f being Face of n
for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f
 n in NAT by ORDINAL1:def_12;
then consider f1 being Function of (NatEmbSeq . n),((FuncsSeq Sk) . n) such that
A60: f1 = F . n and
A61: for x being set st x in NatEmbSeq . n holds
ex m being Nat ex y being Face of m st
( x = y & n = m & ( for s being Element of Sk . (m + 1) st s in Sk . (m + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = f1 . x holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) by A59;
let x be Face of n; ::_thesis: for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,x) = (SgmX ( the InternalRel of C,A)) * x
let s be Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1); ::_thesis: ( s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) implies for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,x) = (SgmX ( the InternalRel of C,A)) * x )
assume A62: s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) ; ::_thesis: for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,x) = (SgmX ( the InternalRel of C,A)) * x
let A be non empty Element of symplexes C; ::_thesis: ( SgmX ( the InternalRel of C,A) = s implies face (s,x) = (SgmX ( the InternalRel of C,A)) * x )
assume A63: SgmX ( the InternalRel of C,A) = s ; ::_thesis: face (s,x) = (SgmX ( the InternalRel of C,A)) * x
A64: ex m being Nat ex y being Face of m st
( x = y & n = m & ( for s being Element of Sk . (m + 1) st s in Sk . (m + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = f1 . x holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) by A61;
 f1 . x in (FuncsSeq Sk) . n ;
then  f1 . x in Funcs ((Sk . (n + 1)),(Sk . n)) by Def3;
then consider G being Function such that
A65: f1 . x = G and
 dom G = Sk . (n + 1) and
 rng G c= Sk . n by FUNCT_2:def_2;
 face (s,x) = G . s by A60, A62, A65, Def7;
hence  face (s,x) = (SgmX ( the InternalRel of C,A)) * x by A62, A63, A64, A65; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict lower_non-empty TriangStr st the SkeletonSeq of b1 . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b1 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) & the SkeletonSeq of b2 . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b2 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) holds
b1 = b2
proof
let T1, T2 be strict lower_non-empty TriangStr ; ::_thesis: ( the SkeletonSeq of T1 . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of T1 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T1 . (n + 1) st s in the SkeletonSeq of T1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) & the SkeletonSeq of T2 . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of T2 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T2 . (n + 1) st s in the SkeletonSeq of T2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) implies T1 = T2 )
assume that
A66: the SkeletonSeq of T1 . 0 = {{}} and
A67: for n being Nat st n > 0 holds
the SkeletonSeq of T1 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  and
A68: for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T1 . (n + 1) st s in the SkeletonSeq of T1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f and
A69: the SkeletonSeq of T2 . 0 = {{}} and
A70: for n being Nat st n > 0 holds
the SkeletonSeq of T2 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  and
A71: for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T2 . (n + 1) st s in the SkeletonSeq of T2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ; ::_thesis: T1 = T2
A72: for x being set st x in NAT holds
the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x
proof
let x be set ; ::_thesis: ( x in NAT implies the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x )
assume  x in NAT ; ::_thesis: the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x
then reconsider n = x as Element of NAT ;
now__::_thesis:_the_SkeletonSeq_of_T1_._n_=_the_SkeletonSeq_of_T2_._n
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n
hence  the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by A66, A69; ::_thesis: verum
end;
supposeA73: n <> 0 ; ::_thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n
then  the SkeletonSeq of T1 . n =  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n  }  by A67;
hence  the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by A70, A73; ::_thesis: verum
end;
end;
end;
hence  the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x ; ::_thesis: verum
end;
then A74: the SkeletonSeq of T1 = the SkeletonSeq of T2 by PBOOLE:3;
now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_
the_FacesAssign_of_T1_._i_=_the_FacesAssign_of_T2_._i
let i be set ; ::_thesis: ( i in NAT implies the FacesAssign of T1 . i = the FacesAssign of T2 . i )
assume  i in NAT ; ::_thesis: the FacesAssign of T1 . i = the FacesAssign of T2 . i
then reconsider n = i as Element of NAT ;
reconsider F1n = the FacesAssign of T1 . n, F2n = the FacesAssign of T2 . n as Function of (NatEmbSeq . n),((FuncsSeq the SkeletonSeq of T1) . n) by A74, PBOOLE:def_15;
A75: dom F2n = NatEmbSeq . n by FUNCT_2:def_1;
A76: now__::_thesis:_for_x_being_set_st_x_in_NatEmbSeq_._n_holds_
F1n_._x_=_F2n_._x
let x be set ; ::_thesis: ( x in NatEmbSeq . n implies F1n . x = F2n . x )
assume  x in NatEmbSeq . n ; ::_thesis: F1n . x = F2n . x
then reconsider x1 = x as Face of n ;
 F1n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ;
then  F1n . x1 in Funcs (( the SkeletonSeq of T1 . (n + 1)),( the SkeletonSeq of T1 . n)) by Def3;
then consider F1nx being Function such that
A77: F1nx = F1n . x1 and
A78: dom F1nx = the SkeletonSeq of T1 . (n + 1) and
 rng F1nx c= the SkeletonSeq of T1 . n by FUNCT_2:def_2;
 F2n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ;
then  F2n . x1 in Funcs (( the SkeletonSeq of T1 . (n + 1)),( the SkeletonSeq of T1 . n)) by Def3;
then consider F2nx being Function such that
A79: F2nx = F2n . x1 and
A80: dom F2nx = the SkeletonSeq of T1 . (n + 1) and
 rng F2nx c= the SkeletonSeq of T1 . n by FUNCT_2:def_2;
now__::_thesis:_for_y_being_set_st_y_in_the_SkeletonSeq_of_T1_._(n_+_1)_holds_
F1nx_._y_=_F2nx_._y
let y be set ; ::_thesis: ( y in the SkeletonSeq of T1 . (n + 1) implies F1nx . y = F2nx . y )
assume A81: y in the SkeletonSeq of T1 . (n + 1) ; ::_thesis: F1nx . y = F2nx . y
then reconsider y1 = y as Symplex of T1,(n + 1) ;
A82: F1nx . y1 = face (y1,x1) by A77, A81, Def7;
reconsider y2 = y as Symplex of T2,(n + 1) by A72, A81;
A83: F2nx . y2 = face (y2,x1) by A74, A79, A81, Def7;
 y1 in  {  (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n + 1  }  by A67, A81;
then consider A being non empty Element of symplexes C such that
A84: SgmX ( the InternalRel of C,A) = y1 and
 card A = n + 1 ;
 face (y1,x1) = (SgmX ( the InternalRel of C,A)) * x1 by A68, A81, A84;
hence  F1nx . y = F2nx . y by A71, A74, A81, A82, A83, A84; ::_thesis: verum
end;
hence  F1n . x = F2n . x by A77, A78, A79, A80, FUNCT_1:2; ::_thesis: verum
end;
 dom F1n = NatEmbSeq . n by FUNCT_2:def_1;
hence  the FacesAssign of T1 . i = the FacesAssign of T2 . i by A75, A76, FUNCT_1:2; ::_thesis: verum
end;
hence  T1 = T2 by A74, PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem  defines Triang TRIANG_1:def_8_:_
 for C being non empty Poset
for b2 being strict lower_non-empty TriangStr holds
( b2 = Triang C iff ( the SkeletonSeq of b2 . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b2 . n =  {  (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n  }  ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) ) );