:: deftheorem defines AddressParts COMPOS_0:def 4 :
for S being non empty standard-ins set
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Element of S : InsCode I = T } ;