let L be lower-bounded sup-Semilattice; :: thesis: for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X
let X be non empty directed Subset of (InclPoset (Ids L)); :: thesis: sup X = union X
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: for x being object st x in X holds
x in bool the carrier of L

let x be object ; :: thesis: ( x in X implies x in bool the carrier of L )
assume x in X ; :: thesis: x in bool the carrier of L
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: verum

end;

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

now :: thesis: for Z being Subset of L st Z in X holds
Z is lower

let Z be Subset of L; :: thesis: ( Z in X implies Z is lower )
assume Z in X ; :: thesis: Z is lower
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: verum

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: for V, Y being Subset of L st V in X & Y in X holds
ex Z being Subset of L st
( Z in X & V \/ Y c= Z )

let V, Y be Subset of L; :: thesis: ( V in X & Y in X implies ex Z being Subset of L st
( Z in X & V \/ Y c= Z ) )
assume A5: ( V in X & Y in X ) ; :: thesis: ex Z being Subset of L st
( Z in X & V \/ Y c= Z )
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: ( Z in X & V \/ Y c= Z )
thus Z in X by A6; :: thesis: V \/ Y c= Z
( V c= Z & Y c= Z ) by A7, YELLOW_1:3;
hence V \/ Y c= Z by XBOOLE_1:8; :: thesis: verum

end;

now :: thesis: for Z being Subset of L st Z in X holds
Z is directed

let Z be Subset of L; :: thesis: ( Z in X implies Z is directed )
assume Z in X ; :: thesis: Z is directed
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: verum

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: for Y being set st Y in X holds
Y c= sup X

let Y be set ; :: thesis: ( Y in X implies Y c= sup X )
assume A8: Y in X ; :: thesis: Y c= sup X
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: verum

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: verum