let L be lower-bounded sup-Semilattice; :: thesis:
let X be non empty directed Subset of (InclPoset (Ids L)); :: thesis:
consider z being object such that
A1: z in X by XBOOLE_0:def 1;
X c= the carrier of (InclPoset (Ids L)) ;
then A2: X c= Ids L by YELLOW_1:1;

now :: thesis:

let x be object ; :: thesis:
assume x in X ; :: thesis:
then x in Ids L by A2;
then x in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then ex x1 being Ideal of L st x = x1 ;
hence x in bool the carrier of L ; :: thesis:

end;

then A3: X c= bool the carrier of L ;

now :: thesis:

let Z be Subset of L; :: thesis:
assume Z in X ; :: thesis:
then Z in Ids L by A2;
then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then ex Z1 being Ideal of L st Z = Z1 ;
hence Z is lower ; :: thesis:

end;

then reconsider unX = union X as lower Subset of L by A3, WAYBEL_0:26;
reconsider z = z as set by TARSKI:1;
z in Ids L by A2, A1;
then z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then ex z1 being Ideal of L st z = z1 ;
then ex v being object st v in z by XBOOLE_0:def 1;
then reconsider unX = unX as non empty lower Subset of L by A1, TARSKI:def 4;

A4: now :: thesis:

let V, Y be Subset of L; :: thesis:
assume A5: ( V in X & Y in X ) ; :: thesis:
then reconsider V1 = V, Y1 = Y as Element of (InclPoset (Ids L)) ;
consider Z1 being Element of (InclPoset (Ids L)) such that
A6: Z1 in X and
A7: ( V1 <= Z1 & Y1 <= Z1 ) by A5, WAYBEL_0:def 1;
Z1 in Ids L by A2, A6;
then Z1 in { Y9 where Y9 is Ideal of L : verum } by WAYBEL_0:def 23;
then ex Z2 being Ideal of L st Z1 = Z2 ;
then reconsider Z = Z1 as Subset of L ;
take Z = Z; :: thesis:
thus Z in X by A6; :: thesis:
( V c= Z & Y c= Z ) by A7, YELLOW_1:3;
hence V \/ Y c= Z by XBOOLE_1:8; :: thesis:

end;

now :: thesis:

let Z be Subset of L; :: thesis:
assume Z in X ; :: thesis:
then Z in Ids L by A2;
then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then ex Z1 being Ideal of L st Z = Z1 ;
hence Z is directed ; :: thesis:

end;

then reconsider unX = unX as non empty directed lower Subset of L by A3, A4, WAYBEL_0:46;
reconsider unX = unX as Element of (InclPoset (Ids L)) by YELLOW_2:41;

now :: thesis:

let Y be set ; :: thesis:
assume A8: Y in X ; :: thesis:
then reconsider Y9 = Y as Element of (InclPoset (Ids L)) ;
sup X is_>=_than X by YELLOW_0:32;
then Y9 <= sup X by A8, LATTICE3:def 9;
hence Y c= sup X by YELLOW_1:3; :: thesis:

end;

then union X c= sup X by ZFMISC_1:76;
then A9: unX <= sup X by YELLOW_1:3;
for b being Element of (InclPoset (Ids L)) st b in X holds
b <= unX by YELLOW_1:3, ZFMISC_1:74;
then unX is_>=_than X by LATTICE3:def 9;
then sup X <= unX by YELLOW_0:32;
hence sup X = union X by A9, ORDERS_2:2; :: thesis: