let L be lower-bounded sup-Semilattice; :: thesis: InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L

now

let x be set ; :: thesis: ( x in Ids L implies x in bool the carrier of L )
assume x in Ids L ; :: thesis: x in bool the carrier of L
then x in { X where X is Ideal of L : verum } by WAYBEL_0:def 23;
then consider x' being Ideal of L such that
A1: x' = x ;
thus x in bool the carrier of L by A1; :: thesis: verum

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

proof

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

now

per cases ( not X is empty or X is empty ) ;

suppose A3: not X is empty ; :: thesis: "/\" X,(BoolePoset the carrier of L) in the carrier of InIdL

X is Subset of (BoolePoset the carrier of L) by Th3;
then A4: "/\" X,(BoolePoset the carrier of L) = meet X by A3, 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 A3, A4, YELLOW_2:47;
then "/\" X,(BoolePoset the carrier of L) is Element of InIdL by YELLOW_2:43;
hence "/\" X,(BoolePoset the carrier of L) in the carrier of InIdL ; :: thesis: verum

end;

suppose A5: X is empty ; :: thesis: "/\" X,(BoolePoset the carrier of L) in the carrier of InIdL

"/\" {} ,(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 A5, YELLOW_2:43;
hence "/\" X,(BoolePoset the carrier of L) in the carrier of InIdL ; :: thesis: verum

end;

end;

end;

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

end;

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

proof

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

now

let z be set ; :: thesis: ( z in X implies z in bool the carrier of L )
assume z in X ; :: thesis: z in bool the carrier of L
then z is Ideal of L by YELLOW_2:43;
hence z in bool the carrier of L ; :: thesis: verum

end;

then A9: X c= bool the carrier of L by TARSKI:def 3;
A10: for Y being Subset of L st Y in X holds
Y is lower by YELLOW_2:43;
A11: for Y being Subset of L st Y in X holds
Y is directed by YELLOW_2:43;

now

let Y, Z be Subset of L; :: thesis: ( Y in X & Z in X implies ex V being Subset of L st
( V in X & Y \/ Z c= V ) )
assume A12: ( Y in X & Z in X ) ; :: thesis: ex V being Subset of L st
( V in X & Y \/ Z c= V )
then reconsider Y' = Y, Z' = Z as Element of InIdL ;
consider V' being Element of InIdL such that
A13: V' in X and
A14: ( Y' <= V' & Z' <= V' ) by A12, WAYBEL_0:def 1;
reconsider V = V' as Subset of L by YELLOW_2:43;
take V = V; :: thesis: ( V in X & Y \/ Z c= V )
thus V in X by A13; :: thesis: Y \/ Z c= V
Y' "\/" Z' <= V' by A14, YELLOW_0:22;
then A15: Y' "\/" Z' c= V' by YELLOW_1:3;
Y \/ Z c= Y' "\/" Z' by YELLOW_1:6;
hence Y \/ Z c= V by A15, XBOOLE_1:1; :: thesis: verum

end;

then uX is Ideal of L by A9, A10, A11, WAYBEL_0:26, WAYBEL_0:46;
then "\/" X,(BoolePoset the carrier of L) is Element of InIdL by A7, YELLOW_2:43;
hence "\/" X,(BoolePoset the carrier of L) in the carrier of InIdL ; :: thesis: verum

end;

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