:: deftheorem Def1 defines Trivial-Mem MEMSTR_0:def 1 :
for N being with_zero set
for b₂ being strict Mem-Struct over N holds
( b₂ = Trivial-Mem N iff ( the carrier of b₂ = {0} & the ZeroF of b₂ = 0 & the Object-Kind of b₂ = 0 .--> 0 & the ValuesF of b₂ = N --> NAT ) );