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 upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)
let J be RelStr-yielding non-Empty ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) implies for i being Element of I holds (Top (product J)) . i = Top (J . i) )
assume A1: for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ; :: thesis: for i being Element of I holds (Top (product J)) . i = Top (J . i)
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = Top (J . $1);
consider f being ManySortedSet of such that
A2: for i being Element of I holds f . i = H₁(i) from PBOOLE:sch 5();
A3: dom f = I by PARTFUN1:def 4;

now

let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = Top (J . i) by A2;
hence f . i is Element of (J . i) ; :: thesis: verum

end;

then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
A4: {} is_>=_than f by YELLOW_0:6;

A5: now

let b be Element of (product J); :: thesis: ( {} is_>=_than b implies f >= b )
assume {} is_>=_than b ; :: thesis: f >= b

now

let i be Element of I; :: thesis: f . i >= b . i
A6: f . i = Top (J . i) by A2;
J . i is non empty antisymmetric upper-bounded RelStr by A1;
hence f . i >= b . i by A6, YELLOW_0:45; :: thesis: verum

end;

hence f >= b by WAYBEL_3:28; :: thesis: verum

end;

now

let c be Element of (product J); :: thesis: ( {} is_>=_than c & ( for b being Element of (product J) st {} is_>=_than b holds
b <= c ) implies c = f )
assume that
{} is_>=_than c and
A7: for b being Element of (product J) st {} is_>=_than b holds
b <= c ; :: thesis: c = f
A8: c >= f by A4, A7;
for i being Element of I holds J . i is antisymmetric by A1;
then A9: product J is antisymmetric by WAYBEL_3:30;

now

let i be Element of I; :: thesis: f . i >= c . i
A10: f . i = Top (J . i) by A2;
J . i is non empty antisymmetric upper-bounded RelStr by A1;
hence f . i >= c . i by A10, YELLOW_0:45; :: thesis: verum

end;

then f >= c by WAYBEL_3:28;
hence c = f by A8, A9, YELLOW_0:def 3; :: thesis: verum

end;

then A11: ex_inf_of {} , product J by A4, A5, YELLOW_0:def 8;

now

let a be Element of (product J); :: thesis: ( {} is_>=_than a implies f >= a )
assume {} is_>=_than a ; :: thesis: f >= a

now

let i be Element of I; :: thesis: f . i >= a . i
A12: f . i = Top (J . i) by A2;
J . i is non empty antisymmetric upper-bounded RelStr by A1;
hence f . i >= a . i by A12, YELLOW_0:45; :: thesis: verum

end;

hence f >= a by WAYBEL_3:28; :: thesis: verum

end;

then A13: f = "/\" {} ,(product J) by A4, A11, YELLOW_0:def 10;
let i be Element of I; :: thesis: (Top (product J)) . i = Top (J . i)
thus (Top (product J)) . i = Top (J . i) by A2, A13; :: thesis: verum