let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of st ( for i being Element of I holds J . i is Semilattice ) holds
product J is with_infima
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies product J is with_infima )
assume A1: for i being Element of I holds J . i is Semilattice ; :: thesis: product J is with_infima
set IT = product J;
for x, y being Element of (product J) ex z being Element of (product J) st
( x >= z & y >= z & ( for z' being Element of (product J) st x >= z' & y >= z' holds
z >= z' ) )

proof

let x, y be Element of (product J); :: thesis: ex z being Element of (product J) st
( x >= z & y >= z & ( for z' being Element of (product J) st x >= z' & y >= z' holds
z >= z' ) )
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = (x . $1) "/\" (y . $1);
consider z being ManySortedSet of such that
A2: for i being Element of I holds z . i = H₁(i) from PBOOLE:sch 5();
A3: dom z = I by PARTFUN1:def 4;
for i being Element of I holds z . i is Element of (J . i)

proof

let i be Element of I; :: thesis: z . i is Element of (J . i)
z . i = (x . i) "/\" (y . i) by A2;
hence z . i is Element of (J . i) ; :: thesis: verum

end;

then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27;
take z ; :: thesis: ( x >= z & y >= z & ( for z' being Element of (product J) st x >= z' & y >= z' holds
z >= z' ) )
for i being Element of I holds
( x . i >= z . i & y . i >= z . i )

proof

let i be Element of I; :: thesis: ( x . i >= z . i & y . i >= z . i )
( J . i is antisymmetric with_infima RelStr & z . i = (x . i) "/\" (y . i) ) by A1, A2;
hence ( x . i >= z . i & y . i >= z . i ) by YELLOW_0:23; :: thesis: verum

end;

hence ( x >= z & y >= z ) by WAYBEL_3:28; :: thesis: for z' being Element of (product J) st x >= z' & y >= z' holds
z >= z'
let z' be Element of (product J); :: thesis: ( x >= z' & y >= z' implies z >= z' )
assume A4: ( x >= z' & y >= z' ) ; :: thesis: z >= z'
for i being Element of I holds z . i >= z' . i

proof

let i be Element of I; :: thesis: z . i >= z' . i
( J . i is antisymmetric with_infima RelStr & x . i >= z' . i & z' . i <= y . i & z . i = (x . i) "/\" (y . i) ) by A1, A2, A4, WAYBEL_3:28;
hence z . i >= z' . i by YELLOW_0:23; :: thesis: verum

end;

hence z >= z' by WAYBEL_3:28; :: thesis: verum

end;

hence product J is with_infima by LATTICE3:def 11; :: thesis: verum