:: deftheorem defines -carrier_of OSALG_4:def 7 :
for R being non empty Poset
for A being ManySortedSet of the carrier of R
for C being Component of R holds A -carrier_of C = union { (A . s) where s is Element of R : s in C } ;