:: deftheorem Def6 defines IC-Ins-separated MEMSTR_0:def 6 :
for N being with_zero set
for IT being non empty Mem-Struct over N holds
( IT is IC-Ins-separated iff Values (IC ) = NAT );