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 lower-bounded RelStr ) holds
product J is lower-bounded
let J be RelStr-yielding non-Empty ManySortedSet of I; :: thesis: ( ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) implies product J is lower-bounded )
assume A1: for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ; :: thesis: product J is lower-bounded
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = Bottom (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 = Bottom (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 4 :: thesis: f is_<=_than the carrier of (product J)
let b be Element of (product J); :: according to LATTICE3:def 8 :: thesis: ( not b in the carrier of (product J) or f <= b )
assume b in the carrier of (product J) ; :: thesis: f <= b

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 = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2;
hence f . i <= b . i by YELLOW_0:44; :: thesis: verum

end;

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