:: deftheorem Def3 defines non-empty MSUALG_1:def 3 :
for S being 1-sorted
for A being many-sorted over S holds
( A is non-empty iff the Sorts of A is V5() );