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: 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)

the InternalRel of (InclPoset (Filt L)) c= the InternalRel of (BoolePoset the carrier of L)

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

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

A5:
field the InternalRel of (InclPoset (Filt L)) = Filt L
by A2, WELLORD2:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (InclPoset (Filt L)) or x in the carrier of (BoolePoset the carrier of L) )

assume x in the carrier of (InclPoset (Filt L)) ; :: thesis: x in the carrier of (BoolePoset the carrier of L)

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: verum

end;assume x in the carrier of (InclPoset (Filt L)) ; :: thesis: x in the carrier of (BoolePoset the carrier of L)

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: verum

the InternalRel of (InclPoset (Filt L)) c= the InternalRel of (BoolePoset the carrier of L)

proof

then reconsider IP = InclPoset (Filt L) as SubRelStr of BoolePoset the carrier of L by A4, YELLOW_0:def 13;
let p be object ; :: 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 A6: p in the InternalRel of (InclPoset (Filt L)) ; :: thesis: p in the InternalRel of (BoolePoset the carrier of L)

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: verum

end;assume A6: p in the InternalRel of (InclPoset (Filt L)) ; :: thesis: p in the InternalRel of (BoolePoset the carrier of L)

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: verum

now :: thesis: for p being object holds

( ( 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)) ) )

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;( ( 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)) ) )

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

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;

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: verum

end;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: ( 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 A19:
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))assume A13:
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 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: verum

end;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: verum

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: verum

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

A24:
IP is directed-sups-inheriting
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Filt L or x in bool the carrier of L )

assume x in Filt L ; :: thesis: x in bool the carrier of L

then ex X being Filter of L st x = X ;

hence x in bool the carrier of L ; :: thesis: verum

end;assume x in Filt L ; :: thesis: x in bool the carrier of L

then ex X being Filter of L st x = X ;

hence x in bool the carrier of L ; :: thesis: verum

proof

IP is infs-inheriting
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 that

A25: X <> {} and

ex_sup_of X, BoolePoset the carrier of L ; :: thesis: "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP

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 )

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 )

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: verum

end;assume that

A25: X <> {} and

ex_sup_of X, BoolePoset the carrier of L ; :: thesis: "\/" (X,(BoolePoset the carrier of L)) in the carrier of IP

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

reconsider X9 = X as Subset of (BoolePoset the carrier of L) by A3, A1, A2, A23, XBOOLE_1:1;
let P, R be Subset of L; :: thesis: ( P in F & R in F implies ex Z being Subset of L st

( Z in F & P \/ R c= Z ) )

assume A28: ( P in F & R in F ) ; :: thesis: ex Z being Subset of L st

( Z in F & P \/ R c= Z )

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: ( Z9 in F & P \/ R c= Z9 )

thus Z9 in F by A29, A31; :: thesis: P \/ R c= Z9

( P9 c= Z & R9 c= Z ) by A30, YELLOW_1:3;

hence P \/ R c= Z9 by A31, XBOOLE_1:8; :: thesis: verum

end;( Z in F & P \/ R c= Z ) )

assume A28: ( P in F & R in F ) ; :: thesis: ex Z being Subset of L st

( Z in F & P \/ R c= Z )

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: ( Z9 in F & P \/ R c= Z9 )

thus Z9 in F by A29, A31; :: thesis: P \/ R c= Z9

( P9 c= Z & R9 c= Z ) by A30, YELLOW_1:3;

hence P \/ R c= Z9 by A31, XBOOLE_1:8; :: thesis: verum

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

then
for X being Subset of L st X in F holds
let X be Subset of L; :: thesis: ( X in F implies ( X is upper & X is filtered ) )

assume X in F ; :: thesis: ( X is upper & X is filtered )

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: verum

end;assume X in F ; :: thesis: ( X is upper & X is filtered )

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: verum

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: verum

proof

hence
InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L
by A24; :: thesis: verum
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));

end;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 )
;

end;

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

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: verum

end;"/\" (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: verum

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

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 )

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

hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A42, A41; :: thesis: verum

end;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

then A41:
sX is filtered
by A39, YELLOW_2:39;
let X be Subset of L; :: thesis: ( X in F implies ( X is upper & X is filtered ) )

assume X in F ; :: thesis: ( X is upper & X is filtered )

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: verum

end;assume X in F ; :: thesis: ( X is upper & X is filtered )

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: verum

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

then
not sX is empty
by A38, A39, SETFAM_1:def 1;
let Y be set ; :: thesis: ( Y in X implies Top L in Y )

assume Y in X ; :: thesis: Top L in Y

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: verum

end;assume Y in X ; :: thesis: Top L in Y

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: verum

hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of IP by A2, A42, A41; :: thesis: verum