theorem :: PCS_0:11

for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) )