:: TRIANG_1  semantic presentation begin  










registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); 
cluster (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  "X" "," "R" "#)" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; 
theorem :: TRIANG_1:1 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k1_xboole_0 :::"{}"::: ) )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: TRIANG_1:2 (Bool  "for" (Set (Var "F")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Bool  "not" (Set (Var "B"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Var "C"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "B")))  ")" )) "holds"  (Bool  "ex" (Set (Var "m")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "m"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "C")))  ")" )  ")" )))) ; 
 registrationlet "P" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "P")); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "P")); 
cluster (Set   ($#k3_orders_2 :::"InitSegm"::: )   "(" "A" "," "x" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; begin  definitionlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); func  :::"symplexes"::: "C" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C") ")" ) equals :: TRIANG_1:def 1  "{"  (Set (Var "A")) where A "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C")) : (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "C")  ($#r3_orders_1 :::"linearly_orders"::: )  (Set (Var "A")))  "}"  ; end; 





:: deftheorem    defines :::"symplexes"::: TRIANG_1:def 1 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::) "holds"  (Bool (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_finsub_1 :::"Fin"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "C")))) : (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "C")))  ($#r3_orders_1 :::"linearly_orders"::: )  (Set (Var "A")))  "}"  )); 
 registrationlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); 
cluster (Set   ($#k1_triang_1 :::"symplexes"::: )  "C") ->   ($#v2_setfam_1 :::"with_non-empty_element"::: )   ; 
end; 



theorem :: TRIANG_1:3 (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds"  (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C")))))) ; 
 
theorem :: TRIANG_1:4 (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C"))))) ; 
 
theorem :: TRIANG_1:5 (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "s")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C")))))) ; 
 
theorem :: TRIANG_1:6 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_pre_poly :::"Element"::: )   "of" (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C")))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "C"))) "," (Set (Var "A")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))))) ; 
 registrationlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_triang_1 :::"symplexes"::: )  "C"); 
end; begin  definitionmode SetSequence is   ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ); end; definitionlet "IT" be   ($#m1_hidden :::"SetSequence":::); attr "IT" is  :::"lower_non-empty":::  means :: TRIANG_1:def 2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Bool  "not" (Set "IT"  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool  "not" (Bool (Set "IT"  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))); end; 




:: deftheorem    defines :::"lower_non-empty"::: TRIANG_1:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"SetSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_triang_1 :::"lower_non-empty"::: )  ) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Bool  "not" (Set (Set (Var "IT"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool  "not" (Bool (Set (Set (Var "IT"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_triang_1 :::"lower_non-empty"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "X" be   ($#m1_hidden :::"SetSequence":::); func  :::"FuncsSeq"::: "X" ->   ($#m1_hidden :::"SetSequence":::) means :: TRIANG_1:def 3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" "X"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" "X"  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))); end; 





:: deftheorem    defines :::"FuncsSeq"::: TRIANG_1:def 3 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "b2")) "being"   ($#m1_hidden :::"SetSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_triang_1 :::"FuncsSeq"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set (Var "X"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))  ")" )); 
 registrationlet "X" be   ($#v1_triang_1 :::"lower_non-empty"::: )    ($#m1_hidden :::"SetSequence":::); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set (Set  "("  ($#k2_triang_1 :::"FuncsSeq"::: )  "X" ")" )  ($#k1_funct_1 :::"."::: )  "n") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Const "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ); func  :::"@"::: "f" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: TRIANG_1:def 4 "f"; end; 






:: deftheorem    defines :::"@"::: TRIANG_1:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) "holds"  (Bool (Set   ($#k3_triang_1 :::"@"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))); 
 definitionfunc  :::"NatEmbSeq":::  ->   ($#m1_hidden :::"SetSequence":::) means :: TRIANG_1:def 5 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "f")) where f "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) : (Bool (Set   ($#k3_triang_1 :::"@"::: )  (Set (Var "f"))) "is"   ($#v5_valued_0 :::"increasing"::: )  )  "}"  )); end; 




:: deftheorem    defines :::"NatEmbSeq"::: TRIANG_1:def 5 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_hidden :::"SetSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_triang_1 :::"NatEmbSeq"::: )  )) "iff" (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "f")) where f "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) : (Bool (Set   ($#k3_triang_1 :::"@"::: )  (Set (Var "f"))) "is"   ($#v5_valued_0 :::"increasing"::: )  )  "}"  ))  ")" )); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set (Set  ($#k4_triang_1 :::"NatEmbSeq"::: ) )  ($#k1_funct_1 :::"."::: )  "n") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k4_triang_1 :::"NatEmbSeq"::: ) )  ($#k1_funct_1 :::"."::: )  "n"); 
end; definitionlet "X" be   ($#m1_hidden :::"SetSequence":::); mode triangulation of "X" is    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set   ($#k4_triang_1 :::"NatEmbSeq"::: )  ) "," (Set   ($#k2_triang_1 :::"FuncsSeq"::: )  "X"); end; definitionattr "c1" is  :::"strict"::: ; struct  :::"TriangStr":::  -> ; aggr :::"TriangStr":::(# :::"SkeletonSeq":::, :::"FacesAssign"::: #) ->    ($#l1_triang_1 :::"TriangStr"::: )  ; sel  :::"SkeletonSeq"::: "c1" ->   ($#m1_hidden :::"SetSequence":::); sel  :::"FacesAssign"::: "c1" ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set   ($#k4_triang_1 :::"NatEmbSeq"::: )  ) "," (Set   ($#k2_triang_1 :::"FuncsSeq"::: )  (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" "c1")); end; definitionlet "T" be    ($#l1_triang_1 :::"TriangStr"::: )  ; attr "T" is  :::"lower_non-empty":::  means :: TRIANG_1:def 6 (Bool (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" "T") "is"   ($#v1_triang_1 :::"lower_non-empty"::: )  ); end; 




:: deftheorem    defines :::"lower_non-empty"::: TRIANG_1:def 6 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_triang_1 :::"TriangStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_triang_1 :::"lower_non-empty"::: )  ) "iff" (Bool (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Var "T"))) "is"   ($#v1_triang_1 :::"lower_non-empty"::: )  )  ")" )); 
 registration
cluster   ($#v2_triang_1 :::"strict"::: )     ($#v3_triang_1 :::"lower_non-empty"::: )    for    ($#l1_triang_1 :::"TriangStr"::: )  ; 
end; registrationlet "T" be   ($#v3_triang_1 :::"lower_non-empty"::: )     ($#l1_triang_1 :::"TriangStr"::: )  ; 
cluster (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" "T") ->   ($#v1_triang_1 :::"lower_non-empty"::: )   ; 
end; registrationlet "S" be   ($#v1_triang_1 :::"lower_non-empty"::: )    ($#m1_hidden :::"SetSequence":::); let "F" be    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set   ($#k4_triang_1 :::"NatEmbSeq"::: )  ) "," (Set   ($#k2_triang_1 :::"FuncsSeq"::: )  (Set (Const "S"))); 
cluster (Set   ($#g1_triang_1 :::"TriangStr"::: )  "(#"  "S" "," "F" "#)" ) ->   ($#v3_triang_1 :::"lower_non-empty"::: )   ; 
end; begin  definitionlet "T" be    ($#l1_triang_1 :::"TriangStr"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); mode Symplex of "T" "," "n" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" "T")  ($#k1_funct_1 :::"."::: )  "n"); end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); mode Face of "n" is    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  ($#k4_triang_1 :::"NatEmbSeq"::: ) )  ($#k1_funct_1 :::"."::: )  "n"); end; definitionlet "T" be   ($#v3_triang_1 :::"lower_non-empty"::: )     ($#l1_triang_1 :::"TriangStr"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); let "x" be   ($#m1_subset_1 :::"Symplex":::) "of" (Set (Const "T")) "," (Set  "(" (Set (Const "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ); let "f" be   ($#m1_subset_1 :::"Face":::) "of" (Set (Const "n")); assume 
(Bool (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Const "T")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Const "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))
 ; func  :::"face":::  "(" "x" "," "f" ")"  ->   ($#m1_subset_1 :::"Symplex":::) "of" "T" "," "n" means :: TRIANG_1:def 7 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_triang_1 :::"FacesAssign"::: )  "of" "T")  ($#k1_funct_1 :::"."::: )  "n")) & (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  "f"))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  "x"))); end; 









:: deftheorem    defines :::"face"::: TRIANG_1:def 7 :  (Bool  "for" (Set (Var "T")) "being"   ($#v3_triang_1 :::"lower_non-empty"::: )     ($#l1_triang_1 :::"TriangStr"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Symplex":::) "of" (Set (Var "T")) "," (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Face":::) "of" (Set (Var "n"))  "st" (Bool (Bool (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Var "T")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Symplex":::) "of" (Set (Var "T")) "," (Set (Var "n")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_triang_1 :::"face"::: )   "(" (Set (Var "x")) "," (Set (Var "f")) ")" )) "iff" (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_triang_1 :::"FacesAssign"::: )  "of" (Set (Var "T")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))  ")" )))))); 
 definitionlet "C" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::); func  :::"Triang"::: "C" ->   ($#v2_triang_1 :::"strict"::: )     ($#v3_triang_1 :::"lower_non-empty"::: )     ($#l1_triang_1 :::"TriangStr"::: )   means :: TRIANG_1:def 8 (Bool  "("  (Bool (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" it)  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" it)  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "C") "," (Set (Var "A")) ")"  ")" ) where A "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_pre_poly :::"Element"::: )   "of" (Set   ($#k1_triang_1 :::"symplexes"::: )  "C") : (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  )  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Face":::) "of" (Set (Var "n"))  (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" it)  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" it)  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_pre_poly :::"Element"::: )   "of" (Set   ($#k1_triang_1 :::"symplexes"::: )  "C")  "st" (Bool (Bool (Set   ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "C") "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k5_triang_1 :::"face"::: )   "(" (Set (Var "s")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "C") "," (Set (Var "A")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))))))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Triang"::: TRIANG_1:def 8 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v2_triang_1 :::"strict"::: )     ($#v3_triang_1 :::"lower_non-empty"::: )     ($#l1_triang_1 :::"TriangStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_triang_1 :::"Triang"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Var "b2")))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Var "b2")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "C"))) "," (Set (Var "A")) ")"  ")" ) where A "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_pre_poly :::"Element"::: )   "of" (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C"))) : (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  )  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Face":::) "of" (Set (Var "n"))  (Bool  "for" (Set (Var "s")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Var "b2")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_triang_1 :::"SkeletonSeq"::: )  "of" (Set (Var "b2")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_pre_poly :::"Element"::: )   "of" (Set   ($#k1_triang_1 :::"symplexes"::: )  (Set (Var "C")))  "st" (Bool (Bool (Set   ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "C"))) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "s")))) "holds"  (Bool (Set   ($#k5_triang_1 :::"face"::: )   "(" (Set (Var "s")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_pre_poly :::"SgmX"::: )   "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "C"))) "," (Set (Var "A")) ")"  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))))))  ")" )  ")" )  ")" )));