let I be set ; :: thesis: 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 ) )
let C be () ManySortedSet of I; :: thesis: 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 ) )
set R = pcs-union C;
let p, q be Element of (pcs-union C); :: thesis: ( 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 ) )
A1: dom (pcs-InternalRels C) = I by PARTFUN1:def 2;
thus ( p <= q implies 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 ) ) :: thesis: ( 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 ) implies p <= q )

proof

assume p <= q ; :: thesis: 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 )
then [p,q] in the InternalRel of (pcs-union C) ;
then [p,q] in Union (pcs-InternalRels C) by Def36;
then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng (pcs-InternalRels C) by TARSKI:def 4;
consider i being object such that
A4: i in dom (pcs-InternalRels C) and
A5: (pcs-InternalRels C) . i = Z by A3, FUNCT_1:def 3;
reconsider I1 = I as non empty set by A4;
reconsider A1 = C as () ManySortedSet of I1 ;
reconsider i1 = i as Element of I1 by A4;
reconsider P = A1 . i1 as pcs-Str ;
take i ; :: thesis: 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 )
take P ; :: thesis: ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 )
Z = the InternalRel of (A1 . i1) by A5, Def6;
then reconsider p9 = p, q9 = q as Element of P by A2, ZFMISC_1:87;
take p9 ; :: thesis: ex q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 )
take q9 ; :: thesis: ( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 )
thus i in I by A4; :: thesis: ( P = C . i & p9 = p & q9 = q & p9 <= q9 )
thus ( P = C . i & p9 = p & q9 = q ) ; :: thesis: p9 <= q9
thus [p9,q9] in the InternalRel of P by A2, A5, Def6; :: according to ORDERS_2:def 5 :: thesis: verum

end;

given i being object , P being pcs-Str , p9, q9 being Element of P such that A6: i in I and
A7: P = C . i and
A8: p9 = p and
A9: q9 = q and
A10: p9 <= q9 ; :: thesis: p <= q
A11: [p9,q9] in the InternalRel of P by A10;
reconsider I1 = I as non empty set by A6;
reconsider i1 = i as Element of I1 by A6;
reconsider A1 = C as () ManySortedSet of I1 ;
(pcs-InternalRels A1) . i1 = the InternalRel of (A1 . i1) by Def6;
then the InternalRel of (A1 . i1) in rng (pcs-InternalRels C) by A1, FUNCT_1:3;
then [p,q] in Union (pcs-InternalRels C) by A7, A8, A9, A11, TARSKI:def 4;
hence [p,q] in the InternalRel of (pcs-union C) by Def36; :: according to ORDERS_2:def 5 :: thesis: verum