let L be lower-bounded sup-Semilattice; :: thesis:

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

end;

then Ids L is Subset-Family of L by TARSKI:def 3;
then reconsider InIdL = InclPoset (Ids L) as non empty full SubRelStr of BoolePoset the carrier of L by YELLOW_1:5;
A1: for X being directed Subset of InIdL st X <> {} & ex_sup_of X, BoolePoset the carrier of L holds
"\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL

let X be directed Subset of InIdL; :: thesis:
assume that
A2: X <> {} and
ex_sup_of X, BoolePoset the carrier of L ; :: thesis:
consider Y being object such that
A3: Y in X by A2, XBOOLE_0:def 1;
X is Subset of (BoolePoset the carrier of L) by Th3;
then A4: "\/" (X,(BoolePoset the carrier of L)) = union X by YELLOW_1:21;
then reconsider uX = union X as Subset of L by WAYBEL_8:26;
reconsider Y = Y as set by TARSKI:1;
Y is Ideal of L by A3, YELLOW_2:41;
then Bottom L in Y by WAYBEL_4:21;
then reconsider uX = uX as non empty Subset of L by A3, TARSKI:def 4;

let z be object ; :: thesis:
assume z in X ; :: thesis:
then z is Ideal of L by YELLOW_2:41;
hence z in bool the carrier of L ; :: thesis:

end;

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

A6: now :: thesis:

let Y, Z be Subset of L; :: thesis:
assume A7: ( Y in X & Z in X ) ; :: thesis:
then reconsider Y9 = Y, Z9 = Z as Element of InIdL ;
consider V9 being Element of InIdL such that
A8: V9 in X and
A9: ( Y9 <= V9 & Z9 <= V9 ) by A7, WAYBEL_0:def 1;
reconsider V = V9 as Subset of L by YELLOW_2:41;
take V = V; :: thesis:
thus V in X by A8; :: thesis:
Y9 "\/" Z9 <= V9 by A9, YELLOW_0:22;
then A10: Y9 "\/" Z9 c= V9 by YELLOW_1:3;
Y \/ Z c= Y9 "\/" Z9 by YELLOW_1:6;
hence Y \/ Z c= V by A10; :: thesis:

end;

( ( for Y being Subset of L st Y in X holds
Y is lower ) & ( for Y being Subset of L st Y in X holds
Y is directed ) ) by YELLOW_2:41;
then uX is Ideal of L by A5, A6, WAYBEL_0:26, WAYBEL_0:46;
then "\/" (X,(BoolePoset the carrier of L)) is Element of InIdL by A4, YELLOW_2:41;
hence "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; :: thesis:

end;

for X being Subset of InIdL st ex_inf_of X, BoolePoset the carrier of L holds
"/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL

let X be Subset of InIdL; :: thesis:
assume ex_inf_of X, BoolePoset the carrier of L ; :: thesis:

suppose A11: not X is empty ; :: thesis:

X is Subset of (BoolePoset the carrier of L) by Th3;
then A12: "/\" (X,(BoolePoset the carrier of L)) = meet X by A11, YELLOW_1:20;
InclPoset (Ids L) = RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def 1;
then "/\" (X,(BoolePoset the carrier of L)) is Ideal of L by A11, A12, YELLOW_2:45;
then "/\" (X,(BoolePoset the carrier of L)) is Element of InIdL by YELLOW_2:41;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; :: thesis:

end;

suppose A13: X is empty ; :: thesis:

"/\" ({},(BoolePoset the carrier of L)) = Top (BoolePoset the carrier of L) by YELLOW_0:def 12
.= the carrier of L by YELLOW_1:19 ;
then "/\" ({},(BoolePoset the carrier of L)) is Ideal of L by Th4;
then "/\" (X,(BoolePoset the carrier of L)) is Element of InIdL by A13, YELLOW_2:41;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; :: thesis:

end;

end;

end;

hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; :: thesis:

end;

hence InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L by A1, WAYBEL_0:def 4, YELLOW_0:def 18; :: thesis: