let L be non empty upper-bounded with_infima Poset; :: thesis:
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: InclPoset (bool the carrier of L) = RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) by YELLOW_1:def 1;
A2: InclPoset (Filt L) = RelStr(# (Filt L),(RelIncl (Filt L)) #) by YELLOW_1:def 1;
A3: BoolePoset the carrier of L = InclPoset (bool the carrier of L) by YELLOW_1:4;
A4: the carrier of (InclPoset (Filt L)) c= the carrier of (BoolePoset the carrier of L)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of (InclPoset (Filt L)) ; :: thesis:
then ex X being Filter of L st x = X by A2;
hence x in the carrier of (BoolePoset the carrier of L) by A3, A1; :: thesis:

end;

A5: field the InternalRel of (InclPoset (Filt L)) = Filt L by A2, WELLORD2:def 1;
the InternalRel of (InclPoset (Filt L)) c= the InternalRel of (BoolePoset the carrier of L)

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: p in the InternalRel of (InclPoset (Filt L)) ; :: thesis:
then consider x, y being object such that
A7: p = [x,y] by RELAT_1:def 1;
A8: y in field the InternalRel of (InclPoset (Filt L)) by A6, A7, RELAT_1:15;
then consider Y being Filter of L such that
A9: y = Y by A5;
A10: x in field the InternalRel of (InclPoset (Filt L)) by A6, A7, RELAT_1:15;
then consider X being Filter of L such that
A11: x = X by A5;
X c= Y by A2, A5, A6, A7, A10, A8, A11, A9, WELLORD2:def 1;
hence p in the InternalRel of (BoolePoset the carrier of L) by A3, A1, A7, A11, A9, WELLORD2:def 1; :: thesis:

end;

then reconsider IP = InclPoset (Filt L) as SubRelStr of BoolePoset the carrier of L by A4, YELLOW_0:def 13;

now :: thesis:

let p be object ; :: thesis:
A12: 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:

assume A13: p in the InternalRel of (InclPoset (Filt L)) ; :: thesis:
then consider x, y being object such that
A14: p = [x,y] by RELAT_1:def 1;
A15: y in field the InternalRel of (InclPoset (Filt L)) by A13, A14, RELAT_1:15;
then consider Y being Filter of L such that
A16: y = Y by A5;
A17: x in field the InternalRel of (InclPoset (Filt L)) by A13, A14, RELAT_1:15;
then consider X being Filter of L such that
A18: x = X by A5;
X c= Y by A2, A5, A13, A14, A17, A15, A18, A16, WELLORD2:def 1;
then p in the InternalRel of (BoolePoset the carrier of L) by A3, A1, A14, A18, A16, WELLORD2:def 1;
hence p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) by A12, A13, XBOOLE_0:def 4; :: thesis:

end;

assume A19: p in the InternalRel of (BoolePoset the carrier of L) |_2 the carrier of (InclPoset (Filt L)) ; :: thesis:
then A20: p in the InternalRel of (BoolePoset the carrier of L) by A12, XBOOLE_0:def 4;
p in [: the carrier of (InclPoset (Filt L)), the carrier of (InclPoset (Filt L)):] by A12, A19, XBOOLE_0:def 4;
then consider x, y being object such that
A21: ( x in the carrier of (InclPoset (Filt L)) & y in the carrier of (InclPoset (Filt L)) ) and
A22: p = [x,y] by ZFMISC_1:def 2;
reconsider x = x, y = y as set by TARSKI:1;
( ex X being Filter of L st x = X & ex Y being Filter of L st y = Y ) by A2, A21;
then x c= y by A3, A1, A20, A22, WELLORD2:def 1;
hence p in the InternalRel of (InclPoset (Filt L)) by A2, A21, A22, WELLORD2:def 1; :: thesis:

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;
A23: Filt L c= bool the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Filt L ; :: thesis:
then ex X being Filter of L st x = X ;
hence x in bool the carrier of L ; :: thesis:

end;

A24: IP is directed-sups-inheriting

proof

let X be directed Subset of IP; :: according to WAYBEL_0:def 4 :: thesis:
assume that
A25: X <> {} and
ex_sup_of X, BoolePoset the carrier of L ; :: thesis:
consider Y being object such that
A26: Y in X by A25, XBOOLE_0:def 1;
reconsider F = X as Subset-Family of the carrier of L by A2, A23, XBOOLE_1:1;
A27: 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 )

proof

let P, R be Subset of L; :: thesis:
assume A28: ( P in F & R in F ) ; :: thesis:
then reconsider P9 = P, R9 = R as Element of IP ;
consider Z being Element of IP such that
A29: Z in X and
A30: ( P9 <= Z & R9 <= Z ) by A28, WAYBEL_0:def 1;
Z in the carrier of IP by A29;
then consider Z9 being Filter of L such that
A31: Z9 = Z by A2;
take Z9 ; :: thesis:
thus Z9 in F by A29, A31; :: thesis:
( P9 c= Z & R9 c= Z ) by A30, YELLOW_1:3;
hence P \/ R c= Z9 by A31, XBOOLE_1:8; :: thesis:

end;

reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
set sX = "\/" (X,(BoolePoset the carrier of L));
A32: sup X9 = union X by YELLOW_1:21;
reconsider sX = "\/" (X,(BoolePoset the carrier of L)) as Subset of L by A1, YELLOW_1:4;
A33: for X being Subset of L st X in F holds
( X is upper & X is filtered )

proof

let X be Subset of L; :: thesis:
assume X in F ; :: thesis:
then X in Filt L by A2;
then ex Y being Filter of L st X = Y ;
hence ( X is upper & X is filtered ) ; :: thesis:

end;

then for X being Subset of L st X in F holds
X is upper ;
then A34: sX is upper by A32, WAYBEL_0:28;
for X being Subset of L st X in F holds
X is filtered by A33;
then A35: sX is filtered by A32, A27, WAYBEL_0:47;
reconsider Y = Y as set by TARSKI:1;
Y in Filt L by A2, A26;
then ex Z being Filter of L st Y = Z ;
then Top L in Y by WAYBEL_4:22;
then not sX is empty by A32, A26, TARSKI:def 4;
hence "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A34, A35; :: thesis:

end;

IP is infs-inheriting

proof

let X be Subset of IP; :: according to YELLOW_0:def 18 :: thesis:
assume ex_inf_of X, BoolePoset the carrier of L ; :: thesis:
set sX = "/\" (X,(BoolePoset the carrier of L));

per cases ;

suppose A36: X is empty ; :: thesis:

A37: [#] L = the carrier of L ;
"/\" (X,(BoolePoset the carrier of L)) = Top (BoolePoset the carrier of L) by A36
.= the carrier of L by YELLOW_1:19 ;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A37; :: thesis:

end;

suppose A38: not X is empty ; :: thesis:

reconsider F = X as Subset-Family of the carrier of L by A2, A23, XBOOLE_1:1;
reconsider sX = "/\" (X,(BoolePoset the carrier of L)) as Subset of L by A1, YELLOW_1:4;
reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
A39: inf X9 = meet X by A38, YELLOW_1:20;
A40: for X being Subset of L st X in F holds
( X is upper & X is filtered )

proof

let X be Subset of L; :: thesis:
assume X in F ; :: thesis:
then X in Filt L by A2;
then ex Y being Filter of L st X = Y ;
hence ( X is upper & X is filtered ) ; :: thesis:

end;

then A41: sX is filtered by A39, YELLOW_2:39;
for X being Subset of L st X in F holds
X is upper by A40;
then A42: sX is upper by A39, YELLOW_2:37;
for Y being set st Y in X holds
Top L in Y

proof

let Y be set ; :: thesis:
assume Y in X ; :: thesis:
then Y in Filt L by A2;
then ex Z being Filter of L st Y = Z ;
hence Top L in Y by WAYBEL_4:22; :: thesis:

end;

then not sX is empty by A38, A39, SETFAM_1:def 1;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A42, A41; :: thesis:

end;

hence InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L by A24; :: thesis: