:: deftheorem defines Triang TRIANG_1:def 8 :
for C being non empty Poset
for b₂ being strict lower_non-empty TriangStr holds
( b₂ = Triang C iff ( the SkeletonSeq of b₂ . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b₂ . 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 b₂ . (n + 1) st s in the SkeletonSeq of b₂ . (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 ) ) );