:: deftheorem defines total SIMPLEX0:def 10 :
for X being set
for KX being SimplicialComplexStr of X holds
( KX is total iff [#] KX = X );