:: deftheorem Def3 defines with_non-empty_values MEMSTR_0:def 3 :
for N being with_zero set
for S being Mem-Struct over N holds
( S is with_non-empty_values iff the_Values_of S is non-empty );