:: deftheorem Def3 defines non-empty UNIALG_1:def 3 :
for IT being UAStr holds
( IT is non-empty iff ( the charact of IT <> {} & the charact of IT is non-empty ) );