let S be lower-bounded sup-Semilattice; :: thesis:
set BS = BoolePoset the carrier of S;
Ids S c= bool the carrier of S

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

end;

then reconsider InIdsS = InclPoset (Ids S) as non empty full SubRelStr of BoolePoset the carrier of S by YELLOW_1:5;
A1: the carrier of InIdsS c= the carrier of (BoolePoset the carrier of S) by YELLOW_0:def 13;

let X be Subset of InIdsS; :: thesis:
assume ex_inf_of X, BoolePoset the carrier of S ; :: thesis:

suppose A2: X <> {} ; :: thesis:

for x being object st x in X holds
x in the carrier of (BoolePoset the carrier of S) by A1;
then X c= the carrier of (BoolePoset the carrier of S) ;
then "/\" (X,(BoolePoset the carrier of S)) = meet X by A2, YELLOW_1:20
.= "/\" (X,InIdsS) by A2, YELLOW_2:46 ;
hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS ; :: thesis:

end;

suppose A3: X = {} ; :: thesis:

"/\" ({},(BoolePoset the carrier of S)) = Top (BoolePoset the carrier of S) by YELLOW_0:def 12
.= the carrier of S by YELLOW_1:19
.= [#] S
.= "/\" ({},InIdsS) by YELLOW_2:47 ;
hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS by A3; :: thesis:

end;

end;

end;

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

end;

then A4: InIdsS is infs-inheriting by YELLOW_0:def 18;

let Y be directed Subset of InIdsS; :: thesis:
assume that
A5: Y <> {} and
ex_sup_of Y, BoolePoset the carrier of S ; :: thesis:
for x being object st x in Y holds
x in the carrier of (BoolePoset the carrier of S) by A1;
then Y c= the carrier of (BoolePoset the carrier of S) ;
then "\/" (Y,(BoolePoset the carrier of S)) = union Y by YELLOW_1:21
.= "\/" (Y,InIdsS) by A5, Th9 ;
hence "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS ; :: thesis:

end;

then InIdsS is directed-sups-inheriting by WAYBEL_0:def 4;
hence InclPoset (Ids S) is algebraic by A4, Th6; :: thesis: