theorem Th12: :: PCS_0:12

for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) )