let I be non empty set ; :: thesis: for C being () ManySortedSet of
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) )
let C be () ManySortedSet of ; :: thesis: for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) )
let p, q be Element of (pcs-union C); :: thesis: ( p (--) q iff ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) )
thus ( p (--) q implies ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) ) :: thesis: ( ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) implies p (--) q )

proof

assume p (--) q ; :: thesis: ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' )
then ex i being set ex P being pcs-Str ex p', q' being Element of P st
( i in I & P = C . i & p' = p & q' = q & p' (--) q' ) by Th12;
hence ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) ; :: thesis: verum

end;

thus ( ex i being Element of I ex p', q' being Element of (C . i) st
( p' = p & q' = q & p' (--) q' ) implies p (--) q ) by Th12; :: thesis: verum