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

A3: now :: thesis: for i being Element of I holds f . i is Element of (J . i)

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;

dom f = I by PARTFUN1:def 2;
then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
take f ; :: according to YELLOW_0:def 5 :: thesis: the carrier of (product J) is_<=_than f
let b be Element of (product J); :: according to LATTICE3:def 9 :: thesis: ( not b in the carrier of (product J) or b <= f )
assume b in the carrier of (product J) ; :: thesis: b <= f

now :: thesis: for i being Element of I holds f . i >= b . i

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

end;

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