defpred S₁[ object , object ] means ex f, g being Function st
( f = $1 & g = $2 & ( 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 ) ) );
consider R being Relation of (product (Carrier J)) such that
A1: for x, y being object holds
( [x,y] in R iff ( x in product (Carrier J) & y in product (Carrier J) & S₁[x,y] ) ) from RELSET_1:sch 1();
take RS = RelStr(# (product (Carrier J)),R #); :: thesis: ( the carrier of RS = product (Carrier J) & ( for x, y being Element of RS 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 ) ) ) ) ) )
thus the carrier of RS = product (Carrier J) ; :: thesis: for x, y being Element of RS 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 ) ) ) )
let x, y be Element of RS; :: thesis: ( x in product (Carrier J) implies ( 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 ) ) ) ) )
assume A2: x in product (Carrier J) ; :: thesis: ( 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 ) ) ) )

hereby :: thesis: ( 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 x <= y )

assume x <= y ; :: thesis: 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 ) ) )
then [x,y] in the InternalRel of RS by ORDERS_2:def 5;
hence 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 A1; :: thesis: verum

end;

assume 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: x <= y
then [x,y] in the InternalRel of RS by A1, A2;
hence x <= y by ORDERS_2:def 5; :: thesis: verum