let L be lower-bounded sup-Semilattice; :: thesis: for A being non empty Subset of (InclPoset (Ids L)) holds
( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )
let A be non empty Subset of (InclPoset (Ids L)); :: thesis: ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )
set P = InclPoset (Ids L);
reconsider A9 = A as non empty Subset of (Ids L) by YELLOW_1:1;
meet A9 is Ideal of L by Th45;
then reconsider I = meet A as Element of (InclPoset (Ids L)) by Th41;
A1: for b being Element of (InclPoset (Ids L)) st b is_<=_than A holds
I >= b

proof

let b be Element of (InclPoset (Ids L)); :: thesis: ( b is_<=_than A implies I >= b )
assume A2: A is_>=_than b ; :: thesis: I >= b
A3: for J being set st J in A holds
b c= J by A2, YELLOW_1:3;
b c= I

proof

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in b or c in I )
assume A4: c in b ; :: thesis: c in I
for J being set st J in A holds
c in J

proof

let J be set ; :: thesis: ( J in A implies c in J )
assume J in A ; :: thesis: c in J
then b c= J by A3;
hence c in J by A4; :: thesis: verum

end;

hence c in I by SETFAM_1:def 1; :: thesis: verum

end;

hence I >= b by YELLOW_1:3; :: thesis: verum

end;

I is_<=_than A

proof

let y be Element of (InclPoset (Ids L)); :: according to LATTICE3:def 8 :: thesis: ( not y in A or I <= y )
assume A5: y in A ; :: thesis: I <= y
I c= y by A5, SETFAM_1:def 1;
hence I <= y by YELLOW_1:3; :: thesis: verum

end;

hence ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A ) by A1, YELLOW_0:31; :: thesis: verum