:: deftheorem defines ObjectKind MEMSTR_0:def 4 :
for N being with_zero set
for S being non empty Mem-Struct over N
for o being Object of S holds ObjectKind o = the Object-Kind of S . o;