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 antisymmetric ) holds
product J is antisymmetric
let J be RelStr-yielding non-Empty ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is antisymmetric ) implies product J is antisymmetric )
assume A1: for i being Element of I holds J . i is antisymmetric ; :: thesis: product J is antisymmetric
let x, y be Element of (product J); :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )
assume that
A2: x <= y and
A3: y <= x ; :: thesis: x = y
A4: dom x = I by Th27;
A5: dom y = I by Th27;

now :: thesis: for j being object st j in I holds
x . j = y . j

let j be object ; :: thesis: ( j in I implies x . j = y . j )
assume j in I ; :: thesis: x . j = y . j
then reconsider i = j as Element of I ;
A6: x . i <= y . i by A2, Th28;
A7: y . i <= x . i by A3, Th28;
J . i is antisymmetric by A1;
hence x . j = y . j by A6, A7; :: thesis: verum

end;

hence x = y by A4, A5, FUNCT_1:2; :: thesis: verum