let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty ManySortedSet of I 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 I; :: 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 that
A2: x <= y and
A3: y <= z ; :: thesis: x <= z
now :: thesis: for i being Element of I holds x . i <= z . i
let i be Element of I; :: thesis: x . i <= z . i
A4: x . i <= y . i by A2, Th28;
A5: y . i <= z . i by A3, Th28;
J . i is transitive by A1;
hence x . i <= z . i by A4, A5; :: thesis: verum
end;
hence x <= z by Th28; :: thesis: verum