:: deftheorem Def2 defines lower_non-empty TRIANG_1:def 2 :
for IT being SetSequence holds
( IT is lower_non-empty iff for n being Nat st not IT . n is empty holds
for m being Nat st m < n holds
not IT . m is empty );