let S1, S2 be strict RelStr ; :: thesis: ( the carrier of S1 = product (Carrier J) & ( for x, y being Element of S1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of S2 = product (Carrier J) & ( for x, y being Element of S2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) implies S1 = S2 )
assume that
A3: the carrier of S1 = product (Carrier J) and
A4: for x, y being Element of S1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) and
A5: the carrier of S2 = product (Carrier J) and
A6: for x, y being Element of S2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ; :: thesis: S1 = S2
the InternalRel of S1 = the InternalRel of S2

proof

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in the InternalRel of S1 or [a,b] in the InternalRel of S2 ) & ( not [a,b] in the InternalRel of S2 or [a,b] in the InternalRel of S1 ) )

hereby :: thesis: ( not [a,b] in the InternalRel of S2 or [a,b] in the InternalRel of S1 )

assume A7: [a,b] in the InternalRel of S1 ; :: thesis: [a,b] in the InternalRel of S2
then reconsider x = a, y = b as Element of S1 by ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of S2 by A3, A5;
A8: a in the carrier of S1 by A7, ZFMISC_1:87;
x <= y by A7, ORDERS_2:def 5;
then ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A3, A4, A8;
then x9 <= y9 by A3, A6, A8;
hence [a,b] in the InternalRel of S2 by ORDERS_2:def 5; :: thesis: verum

end;

assume A9: [a,b] in the InternalRel of S2 ; :: thesis: [a,b] in the InternalRel of S1
then reconsider x = a, y = b as Element of S2 by ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of S1 by A3, A5;
A10: a in the carrier of S2 by A9, ZFMISC_1:87;
x <= y by A9, ORDERS_2:def 5;
then ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A5, A6, A10;
then x9 <= y9 by A4, A5, A10;
hence [a,b] in the InternalRel of S1 by ORDERS_2:def 5; :: thesis: verum

end;

hence S1 = S2 by A3, A5; :: thesis: verum