:: deftheorem defines proj WAYBEL18:def 4 :
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) = proj ((Carrier J),i);