let L be lower-bounded sup-Semilattice; :: thesis: for X being non empty Subset of (Ids L) holds meet X is Ideal of L
let X be non empty Subset of (Ids L); :: thesis: meet X is Ideal of L
A1: for J being set st J in X holds
J is Ideal of L

proof

let J be set ; :: thesis: ( J in X implies J is Ideal of L )
assume J in X ; :: thesis: J is Ideal of L
then J in Ids L ;
then ex Y being Ideal of L st Y = J ;
hence J is Ideal of L ; :: thesis: verum

end;

X c= bool the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in bool the carrier of L )
assume x in X ; :: thesis: x in bool the carrier of L
then x is Ideal of L by A1;
hence x in bool the carrier of L ; :: thesis: verum

end;

then reconsider F = X as Subset-Family of L ;
for J being Subset of L st J in F holds
J is lower by A1;
then reconsider I = meet X as lower Subset of L by Th36;
for J being set st J in X holds
Bottom L in J

proof

let J be set ; :: thesis: ( J in X implies Bottom L in J )
assume J in X ; :: thesis: Bottom L in J
then reconsider J9 = J as Ideal of L by A1;
set j = the Element of J9;
Bottom L <= the Element of J9 by YELLOW_0:44;
hence Bottom L in J by WAYBEL_0:def 19; :: thesis: verum

end;

then reconsider I = I as non empty lower Subset of L by SETFAM_1:def 1;
for J being Subset of L st J in F holds
( J is lower & J is directed ) by A1;
then I is Ideal of L by Th38;
hence meet X is Ideal of L ; :: thesis: verum