begin
begin
begin
begin
definition
let C be non
empty Poset;
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 ) )
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
end;