let S be lower-bounded sup-Semilattice; :: thesis: InclPoset (Ids S) is algebraic
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 consider x1 being Ideal of S such that
A1: x = x1 ;
thus x in bool the carrier of S by A1; :: thesis: verum

end;

then reconsider InIdsS = InclPoset (Ids S) as non empty full SubRelStr of BoolePoset the carrier of S by YELLOW_1:5;
set BS = BoolePoset the carrier of S;
A2: 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 A3: 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 A2; :: 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 A3, YELLOW_1:20
.= "/\" X,InIdsS by A3, YELLOW_2:48 ;
hence "/\" X,(BoolePoset the carrier of S) in the carrier of InIdsS ; :: thesis: verum

end;

suppose A4: 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:49 ;
hence "/\" X,(BoolePoset the carrier of S) in the carrier of InIdsS by A4; :: thesis: verum

end;

end;

end;

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

end;

then A5: 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
A6: 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 A2; :: 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 A6, 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 A5, Th6; :: thesis: verum