let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty ManySortedSet of st ( for i being Element of I holds J . i is transitive ) holds
product J is transitive
let J be RelStr-yielding non-Empty ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is transitive ) implies product J is transitive )
assume A1: for i being Element of I holds J . i is transitive ; :: thesis: product J is transitive
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 A2: ( x <= y & y <= z ) ; :: thesis: x <= z

now

let i be Element of I; :: thesis: x . i <= z . i
( x . i <= y . i & y . i <= z . i & J . i is transitive ) by A1, A2, Th28;
hence x . i <= z . i by YELLOW_0:def 2; :: thesis: verum

end;

hence x <= z by Th28; :: thesis: verum