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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ids S or x in bool the carrier of S )
assume x in Ids S ; :: thesis: x in bool the carrier of S
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: verum

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;

now :: thesis: for X being Subset of InIdsS st ex_inf_of X, BoolePoset the carrier of S holds
"/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS

let X be Subset of InIdsS; :: thesis: ( ex_inf_of X, BoolePoset the carrier of S implies "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS )
assume ex_inf_of X, BoolePoset the carrier of S ; :: thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS

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

per cases ( X <> {} or X = {} ) ;

suppose A2: X <> {} ; :: thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS

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

end;

suppose A3: X = {} ; :: thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS

"/\" ({},(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: verum

end;

end;

end;

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

end;

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

now :: thesis: for Y being directed Subset of InIdsS st Y <> {} & ex_sup_of Y, BoolePoset the carrier of S holds
"\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS

let Y be directed Subset of InIdsS; :: thesis: ( Y <> {} & ex_sup_of Y, BoolePoset the carrier of S implies "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS )
assume that
A5: Y <> {} and
ex_sup_of Y, BoolePoset the carrier of S ; :: thesis: "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS
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: verum

end;

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