:: 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 } ;