theorem Th5: :: OSALG_4:5

for R being non empty Poset
for A being ManySortedSet of the carrier of R
for s being Element of R
for x being set st x in A . s holds
x in A -carrier_of (CComp s)