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 Th47;
then reconsider I = meet A as Element of (InclPoset (Ids L)) by Th43;
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

proof

let J be set ; :: thesis: ( J in A implies b c= J )
assume A4: J in A ; :: thesis: b c= J
then reconsider y = J as Element of (InclPoset (Ids L)) ;
b <= y by A2, A4, LATTICE3:def 8;
hence b c= J by YELLOW_1:3; :: thesis: verum

end;

b c= I

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in b or c in I )
assume A5: 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 A5; :: 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 A6: y in A ; :: thesis: I <= y
I c= y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in I or x in y )
assume x in I ; :: thesis: x in y
hence x in y by A6, SETFAM_1:def 1; :: thesis: verum

end;

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