:: deftheorem Def11 defines Net-Str WAYBEL11:def 11 :
for S being non empty 1-sorted
for e being Element of S
for b₃ being strict NetStr over S holds
( b₃ = Net-Str e iff ( the carrier of b₃ = {e} & the InternalRel of b₃ = {[e,e]} & the mapping of b₃ = id {e} ) );