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 set ; :: 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

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

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

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

now

let x be set ; :: thesis: ( x in X implies x in the carrier of (BoolePoset the carrier of S) )
assume x in X ; :: thesis: x in the carrier of (BoolePoset the carrier of S)
then x in the carrier of InIdsS ;
hence x in the carrier of (BoolePoset the carrier of S) by A1; :: thesis: verum

end;

then X c= the carrier of (BoolePoset the carrier of S) by TARSKI:def 3;
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

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

now

let x be set ; :: thesis: ( x in Y implies x in the carrier of (BoolePoset the carrier of S) )
assume x in Y ; :: thesis: x in the carrier of (BoolePoset the carrier of S)
then x in the carrier of InIdsS ;
hence x in the carrier of (BoolePoset the carrier of S) by A1; :: thesis: verum

end;

then Y c= the carrier of (BoolePoset the carrier of S) by TARSKI:def 3;
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