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 Th10;
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 Th10; :: thesis: verum