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 antisymmetric ) holds
product J is antisymmetric
let J be RelStr-yielding non-Empty ManySortedSet of ; :: 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 A2: ( x <= y & y <= x ) ; :: thesis: x = y
A3: ( dom x = I & dom y = I ) by Th27;

now

let j be set ; :: 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 ;
( x . i <= y . i & y . i <= x . i & J . i is antisymmetric ) by A1, A2, Th28;
hence x . j = y . j by YELLOW_0:def 3; :: thesis: verum

end;

hence x = y by A3, FUNCT_1:9; :: thesis: verum