let L be lower-bounded sup-Semilattice; :: thesis: InclPoset (Ids L) is CLSubFrame of
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 x' being Ideal of L st x' = x ;
hence x in bool the carrier of L ; :: thesis: verum
end;
then Ids L is Subset-Family of 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 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 ; :: 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 by Th3;
then A4: "\/" X,(BoolePoset the carrier of L) = union X by YELLOW_1:21;
then reconsider uX = union X as Subset of 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 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 ; :: thesis: ( Y in X & Z in X implies ex V being Subset of st
( V in X & Y \/ Z c= V ) )
assume A7: ( Y in X & Z in X ) ; :: thesis: ex V being Subset of st
( V in X & Y \/ Z c= V )
then reconsider Y' = Y, Z' = Z as Element of ;
consider V' being Element of such that
A8: V' in X and
A9: ( Y' <= V' & Z' <= V' ) by A7, WAYBEL_0:def 1;
reconsider V = V' as Subset of 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
Y' "\/" Z' <= V' by A9, YELLOW_0:22;
then A10: Y' "\/" Z' c= V' by YELLOW_1:3;
Y \/ Z c= Y' "\/" Z' by YELLOW_1:6;
hence Y \/ Z c= V by A10, XBOOLE_1:1; :: thesis: verum
end;
( ( for Y being Subset of st Y in X holds
Y is lower ) & ( for Y being Subset of 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 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 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 ; :: 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 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 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 by A1, WAYBEL_0:def 4, YELLOW_0:def 18; :: thesis: verum