let I be non empty set ; :: thesis: 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 ) )
let C be () ManySortedSet of I; :: thesis: 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 ) )
let p, q be Element of (pcs-union C); :: thesis: ( p <= q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) )
thus ( p <= q implies ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) ) :: thesis: ( ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) implies p <= q )

proof

assume p <= q ; :: thesis: ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 )
then ex i being set 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 ) by Th10;
hence ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) ; :: thesis: verum

end;

thus ( ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) implies p <= q ) by Th10; :: thesis: verum