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
X c= the carrier of (InclPoset (Ids L)) ;
then A1: X c= Ids L by YELLOW_1:1;

now

let x be set ; :: 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 A1;
then x in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then consider x1 being Ideal of L such that
A2: x = x1 ;
thus x in bool the carrier of L by A2; :: thesis: verum

end;

then A3: X c= bool the carrier of L by TARSKI:def 3;

now

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 A1;
then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then consider Z1 being Ideal of L such that
A4: Z = Z1 ;
thus Z is lower by A4; :: thesis: verum

end;

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

A8: now

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 A1;
then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def 23;
then consider Z1 being Ideal of L such that
A9: Z = Z1 ;
thus Z is directed by A9; :: thesis: verum

end;

now

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 that
A10: V in X and
A11: Y in X ; :: thesis: ex Z being Subset of L st
( Z in X & V \/ Y c= Z )
reconsider V1 = V, Y1 = Y as Element of (InclPoset (Ids L)) by A10, A11;
consider Z1 being Element of (InclPoset (Ids L)) such that
A12: Z1 in X and
A13: V1 <= Z1 and
A14: Y1 <= Z1 by A10, A11, WAYBEL_0:def 1;
Z1 in Ids L by A1, A12;
then Z1 in { Y' where Y' is Ideal of L : verum } by WAYBEL_0:def 23;
then consider Z2 being Ideal of L such that
A15: Z1 = Z2 ;
reconsider Z = Z1 as Subset of L by A15;
take Z = Z; :: thesis: ( Z in X & V \/ Y c= Z )
thus Z in X by A12; :: thesis: V \/ Y c= Z
( V c= Z & Y c= Z ) by A13, A14, YELLOW_1:3;
hence V \/ Y c= Z by XBOOLE_1:8; :: thesis: verum

end;

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

now

let b be Element of (InclPoset (Ids L)); :: thesis: ( b in X implies b <= unX )
assume b in X ; :: thesis: b <= unX
then b c= union X by ZFMISC_1:92;
hence b <= unX by YELLOW_1:3; :: thesis: verum

end;

then unX is_>=_than X by LATTICE3:def 9;
then A16: sup X <= unX by YELLOW_0:32;

now

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

end;

then union X c= sup X by ZFMISC_1:94;
then unX <= sup X by YELLOW_1:3;
hence sup X = union X by A16, ORDERS_2:25; :: thesis: verum