:: deftheorem Def6 defines lower_non-empty TRIANG_1:def 6 :
for T being TriangStr holds
( T is lower_non-empty iff the SkeletonSeq of T is lower_non-empty );