A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
thus product J is directed :: thesis: product J is transitive

proof

let x, y be Element of (product J); :: according to YELLOW_6:def 5 :: thesis: ex z being Element of (product J) st
( x <= z & y <= z )
defpred S₁[ Element of Y, set ] means ( [(x . T),Y] in the InternalRel of (J . T) & [(y . T),Y] in the InternalRel of (J . T) );

A2: now

let i be Element of Y; :: thesis: ex z being set st S₁[i,z]
consider zi being Element of (J . i) such that
A3: ( x . i <= zi & y . i <= zi ) by Def5;
reconsider z = zi as set ;
take z = z; :: thesis: S₁[i,z]
thus S₁[i,z] by A3, ORDERS_2:def 9; :: thesis: verum

end;

consider z being ManySortedSet of such that
A4: for i being Element of Y holds S₁[i,z . i] from PBOOLE:sch 6(A2);
A5: dom z = the carrier of Y by PARTFUN1:def 4
.= dom (Carrier J) by PARTFUN1:def 4 ;

now

let i be set ; :: thesis: ( i in dom (Carrier J) implies z . i in (Carrier J) . i )
assume i in dom (Carrier J) ; :: thesis: z . i in (Carrier J) . i
then reconsider j = i as Element of Y by PARTFUN1:def 4;
[(x . j),(z . j)] in the InternalRel of (J . j) by A4;
then z . j in the carrier of (J . j) by ZFMISC_1:106;
hence z . i in (Carrier J) . i by Th9; :: thesis: verum

end;

then reconsider z = z as Element of (product J) by A1, A5, CARD_3:18;
take z ; :: thesis: ( x <= z & y <= z )
for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )

proof

let i be set ; :: thesis: ( i in the carrier of Y implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi ) )
assume i in the carrier of Y ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
then reconsider j = i as Element of Y ;
reconsider xi = x . j, zi = z . j as Element of (J . j) ;
take J . j ; :: thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take zi ; :: thesis: ( J . j = J . i & xi = x . i & zi = z . i & xi <= zi )
thus ( J . j = J . i & xi = x . i & zi = z . i ) ; :: thesis: xi <= zi
[xi,zi] in the InternalRel of (J . j) by A4;
hence xi <= zi by ORDERS_2:def 9; :: thesis: verum

end;

hence x <= z by A1, YELLOW_1:def 4; :: thesis: y <= z
for i being set st i in the carrier of Y holds
ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi )

proof

let i be set ; :: thesis: ( i in the carrier of Y implies ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi ) )
assume i in the carrier of Y ; :: thesis: ex R being RelStr ex yi, zi being Element of R st
( R = J . i & yi = y . i & zi = z . i & yi <= zi )
then reconsider j = i as Element of Y ;
reconsider yi = y . j, zi = z . j as Element of (J . j) ;
take J . j ; :: thesis: ex yi, zi being Element of (J . j) st
( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
take yi ; :: thesis: ex zi being Element of (J . j) st
( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
take zi ; :: thesis: ( J . j = J . i & yi = y . i & zi = z . i & yi <= zi )
thus ( J . j = J . i & yi = y . i & zi = z . i ) ; :: thesis: yi <= zi
[yi,zi] in the InternalRel of (J . j) by A4;
hence yi <= zi by ORDERS_2:def 9; :: thesis: verum

end;

hence y <= z by A1, YELLOW_1:def 4; :: thesis: verum

end;

let x, y, z be Element of (product J); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A6: x <= y and
A7: y <= z ; :: thesis: x <= z
consider fx, gy being Function such that
A8: ( fx = x & gy = y ) and
A9: for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = fx . i & yi = gy . i & xi <= yi ) by A1, A6, YELLOW_1:def 4;
consider fy, gz being Function such that
A10: ( fy = y & gz = z ) and
A11: for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = fy . i & yi = gz . i & xi <= yi ) by A1, A7, YELLOW_1:def 4;
for i being set st i in the carrier of Y holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )

proof

let i be set ; :: thesis: ( i in the carrier of Y implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi ) )
assume A12: i in the carrier of Y ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = z . i & xi <= yi )
then reconsider j = i as Element of Y ;
consider R1 being RelStr , xi, yi being Element of R1 such that
A13: ( R1 = J . i & xi = x . i & yi = y . i & xi <= yi ) by A8, A9, A12;
consider R2 being RelStr , yi', zi being Element of R2 such that
A14: ( R2 = J . i & yi' = y . i & zi = z . i & yi' <= zi ) by A10, A11, A12;
reconsider xi = xi, zi = zi as Element of (J . j) by A13, A14;
take J . j ; :: thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of (J . j) st
( J . j = J . i & xi = x . i & yi = z . i & xi <= yi )
take zi ; :: thesis: ( J . j = J . i & xi = x . i & zi = z . i & xi <= zi )
thus ( J . j = J . i & xi = x . i & zi = z . i ) by A13, A14; :: thesis: xi <= zi
thus xi <= zi by A13, A14, YELLOW_0:def 2; :: thesis: verum

end;

hence x <= z by A1, YELLOW_1:def 4; :: thesis: verum