:: deftheorem defines ProjMap TOPS_5:def 3 :
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I holds ProjMap J = ProjMap (Carrier J);