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 ex x9 being Ideal of L st x9 = x ;
hence x in bool the carrier of L ; :: 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;
A1: 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
A2: X <> {} and
ex_sup_of X, BoolePoset the carrier of L ; :: thesis: "\/" X,(BoolePoset the carrier of L) in the carrier of InIdL
consider Y being set such that
A3: Y in X by A2, XBOOLE_0:def 1;
X is Subset of (BoolePoset the carrier of L) by Th3;
then A4: "\/" 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;
Y is Ideal of L by A3, YELLOW_2:43;
then Bottom L in Y by WAYBEL_4:21;
then reconsider uX = uX as non empty Subset of L by A3, 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 A5: X c= bool the carrier of L by TARSKI:def 3;

A6: 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 A7: ( Y in X & Z in X ) ; :: thesis: ex V being Subset of L st
( V in X & Y \/ Z c= V )
then reconsider Y9 = Y, Z9 = Z as Element of InIdL ;
consider V9 being Element of InIdL such that
A8: V9 in X and
A9: ( Y9 <= V9 & Z9 <= V9 ) by A7, WAYBEL_0:def 1;
reconsider V = V9 as Subset of L by YELLOW_2:43;
take V = V; :: thesis: ( V in X & Y \/ Z c= V )
thus V in X by A8; :: thesis: Y \/ Z c= V
Y9 "\/" Z9 <= V9 by A9, YELLOW_0:22;
then A10: Y9 "\/" Z9 c= V9 by YELLOW_1:3;
Y \/ Z c= Y9 "\/" Z9 by YELLOW_1:6;
hence Y \/ Z c= V by A10, XBOOLE_1:1; :: thesis: verum

end;

( ( for Y being Subset of L st Y in X holds
Y is lower ) & ( for Y being Subset of L st Y in X holds
Y is directed ) ) by YELLOW_2:43;
then uX is Ideal of L by A5, A6, WAYBEL_0:26, WAYBEL_0:46;
then "\/" X,(BoolePoset the carrier of L) is Element of InIdL by A4, YELLOW_2:43;
hence "\/" X,(BoolePoset the carrier of L) in the carrier of InIdL ; :: thesis: verum

end;

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 A11: 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 A12: "/\" X,(BoolePoset the carrier of L) = meet X by A11, 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 A11, A12, 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 A13: 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 A13, 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;

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