let L be non empty upper-bounded with_infima Poset; :: thesis: InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
set cL = the carrier of L;
set BP = BoolePoset the carrier of L;
set cBP = the carrier of (BoolePoset the carrier of L);
set rBP = the InternalRel of (BoolePoset the carrier of L);
set IP = InclPoset (Filt L);
set cIP = the carrier of (InclPoset (Filt L));
set rIP = the InternalRel of (InclPoset (Filt L));
A1:
BoolePoset the carrier of L = InclPoset (bool the carrier of L)
by YELLOW_1:4;
A2:
InclPoset (bool the carrier of L) = RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #)
by YELLOW_1:def 1;
A3:
InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #)
by YELLOW_1:def 1;
then A4:
field the InternalRel of (InclPoset (Filt L)) = Filt L
by WELLORD2:def 1;
A5:
Filt L c= bool the carrier of L
A7:
the carrier of (InclPoset (Filt L)) c= the carrier of (BoolePoset the carrier of L)
the InternalRel of (InclPoset (Filt L)) c= the InternalRel of (BoolePoset the carrier of L)
proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in the InternalRel of (InclPoset (Filt L)) or p in the InternalRel of (BoolePoset the carrier of L) )
assume A9:
p in the
InternalRel of
(InclPoset (Filt L))
;
:: thesis: p in the InternalRel of (BoolePoset the carrier of L)
then consider x,
y being
set such that A10:
p = [x,y]
by RELAT_1:def 1;
A11:
(
x in field the
InternalRel of
(InclPoset (Filt L)) &
y in field the
InternalRel of
(InclPoset (Filt L)) )
by A9, A10, RELAT_1:30;
then consider X being
Filter of
L such that A12:
x = X
by A4;
consider Y being
Filter of
L such that A13:
y = Y
by A4, A11;
X c= Y
by A3, A4, A9, A10, A11, A12, A13, WELLORD2:def 1;
hence
p in the
InternalRel of
(BoolePoset the carrier of L)
by A1, A2, A10, A12, A13, WELLORD2:def 1;
:: thesis: verum
end;
then reconsider IP = InclPoset (Filt L) as SubRelStr of BoolePoset the carrier of L by A7, YELLOW_0:def 13;
now let p be
set ;
:: thesis: ( ( p in the InternalRel of (InclPoset (Filt L)) implies p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) ) & ( p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) implies p in the InternalRel of (InclPoset (Filt L)) ) )A14:
the
InternalRel of
(BoolePoset the carrier of L) |_2 the
carrier of
(InclPoset (Filt L)) = the
InternalRel of
(BoolePoset the carrier of L) /\ [:the carrier of (InclPoset (Filt L)),the carrier of (InclPoset (Filt L)):]
by WELLORD1:def 6;
hereby :: thesis: ( p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) implies p in the InternalRel of (InclPoset (Filt L)) )
assume A15:
p in the
InternalRel of
(InclPoset (Filt L))
;
:: thesis: p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L))then consider x,
y being
set such that A16:
p = [x,y]
by RELAT_1:def 1;
A17:
(
x in field the
InternalRel of
(InclPoset (Filt L)) &
y in field the
InternalRel of
(InclPoset (Filt L)) )
by A15, A16, RELAT_1:30;
then consider X being
Filter of
L such that A18:
x = X
by A4;
consider Y being
Filter of
L such that A19:
y = Y
by A4, A17;
X c= Y
by A3, A4, A15, A16, A17, A18, A19, WELLORD2:def 1;
then
p in the
InternalRel of
(BoolePoset the carrier of L)
by A1, A2, A16, A18, A19, WELLORD2:def 1;
hence
p in the
InternalRel of
(BoolePoset the carrier of L) |_2 the
carrier of
(InclPoset (Filt L))
by A14, A15, XBOOLE_0:def 4;
:: thesis: verum
end; assume
p in the
InternalRel of
(BoolePoset the carrier of L) |_2 the
carrier of
(InclPoset (Filt L))
;
:: thesis: p in the InternalRel of (InclPoset (Filt L))then A20:
(
p in the
InternalRel of
(BoolePoset the carrier of L) &
p in [:the carrier of (InclPoset (Filt L)),the carrier of (InclPoset (Filt L)):] )
by A14, XBOOLE_0:def 4;
then consider x,
y being
set such that A21:
(
x in the
carrier of
(InclPoset (Filt L)) &
y in the
carrier of
(InclPoset (Filt L)) &
p = [x,y] )
by ZFMISC_1:def 2;
consider X being
Filter of
L such that A22:
x = X
by A3, A21;
consider Y being
Filter of
L such that A23:
y = Y
by A3, A21;
x c= y
by A1, A2, A20, A21, A22, A23, WELLORD2:def 1;
hence
p in the
InternalRel of
(InclPoset (Filt L))
by A3, A21, WELLORD2:def 1;
:: thesis: verum end;
then
the InternalRel of (InclPoset (Filt L)) = the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L))
by TARSKI:2;
then reconsider IP = IP as full SubRelStr of BoolePoset the carrier of L by YELLOW_0:def 14;
A24:
IP is infs-inheriting
proof
let X be
Subset of
IP;
:: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of X, BoolePoset the carrier of L or "/\" X,(BoolePoset the carrier of L) in the carrier of IP )
assume
ex_inf_of X,
BoolePoset the
carrier of
L
;
:: thesis: "/\" X,(BoolePoset the carrier of L) in the carrier of IP
set sX =
"/\" X,
(BoolePoset the carrier of L);
per cases
( X is empty or not X is empty )
;
suppose A26:
not
X is
empty
;
:: thesis: "/\" X,(BoolePoset the carrier of L) in the carrier of IPreconsider X' =
X as
Subset of
(BoolePoset the carrier of L) by A1, A2, A3, A5, XBOOLE_1:1;
reconsider F =
X as
Subset-Family of the
carrier of
L by A3, A5, XBOOLE_1:1;
A27:
inf X' = meet X
by A26, YELLOW_1:20;
reconsider sX =
"/\" X,
(BoolePoset the carrier of L) as
Subset of
L by A2, YELLOW_1:4;
for
Y being
set st
Y in X holds
Top L in Y
then A29:
not
sX is
empty
by A26, A27, SETFAM_1:def 1;
A30:
for
X being
Subset of
L st
X in F holds
(
X is
upper &
X is
filtered )
then
for
X being
Subset of
L st
X in F holds
X is
upper
;
then A33:
sX is
upper
by A27, YELLOW_2:39;
sX is
filtered
by A27, A30, YELLOW_2:41;
hence
"/\" X,
(BoolePoset the carrier of L) in the
carrier of
IP
by A3, A29, A33;
:: thesis: verum end;
end;
IP is directed-sups-inheriting
proof
let X be
directed Subset of
IP;
:: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X, BoolePoset the carrier of L or "\/" X,(BoolePoset the carrier of L) in the carrier of IP )
assume A34:
(
X <> {} &
ex_sup_of X,
BoolePoset the
carrier of
L )
;
:: thesis: "\/" X,(BoolePoset the carrier of L) in the carrier of IP
set sX =
"\/" X,
(BoolePoset the carrier of L);
reconsider X' =
X as
Subset of
(BoolePoset the carrier of L) by A1, A2, A3, A5, XBOOLE_1:1;
reconsider F =
X as
Subset-Family of the
carrier of
L by A3, A5, XBOOLE_1:1;
A35:
sup X' = union X
by YELLOW_1:21;
reconsider sX =
"\/" X,
(BoolePoset the carrier of L) as
Subset of
L by A2, YELLOW_1:4;
consider Y being
set such that A36:
Y in X
by A34, XBOOLE_0:def 1;
Y in Filt L
by A3, A36;
then consider Z being
Filter of
L such that A37:
Y = Z
;
Top L in Y
by A37, WAYBEL_4:22;
then A38:
not
sX is
empty
by A35, A36, TARSKI:def 4;
A39:
for
X being
Subset of
L st
X in F holds
(
X is
upper &
X is
filtered )
then
for
X being
Subset of
L st
X in F holds
X is
upper
;
then A41:
sX is
upper
by A35, WAYBEL_0:28;
A42:
for
X being
Subset of
L st
X in F holds
X is
filtered
by A39;
for
P,
R being
Subset of
L st
P in F &
R in F holds
ex
Z being
Subset of
L st
(
Z in F &
P \/ R c= Z )
then
sX is
filtered
by A35, A42, WAYBEL_0:47;
hence
"\/" X,
(BoolePoset the carrier of L) in the
carrier of
IP
by A3, A38, A41;
:: thesis: verum
end;
hence
InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
by A24; :: thesis: verum