let X, E be set ; for L being CLSubFrame of BoolePoset X holds
( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
let L be CLSubFrame of BoolePoset X; ( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
A1:
the carrier of L c= the carrier of (BoolePoset X)
by YELLOW_0:def 13;
A2:
L is complete LATTICE
by YELLOW_2:30;
thus
( E in the carrier of (CompactSublatt L) implies ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
( ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of (CompactSublatt L) )proof
A3:
(closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) =
[#] (CompactSublatt (Image (closure_op L)))
by WAYBEL_8:25
.=
[#] (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #))
by WAYBEL10:18
.=
the
carrier of
(CompactSublatt RelStr(# the carrier of L, the InternalRel of L #))
;
assume
E in the
carrier of
(CompactSublatt L)
;
ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E )
then
E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X)))
by A2, A3, Th5;
then consider x being
object such that A4:
x in dom (closure_op L)
and A5:
x in [#] (CompactSublatt (BoolePoset X))
and A6:
E = (closure_op L) . x
by FUNCT_1:def 6;
reconsider F =
x as
Element of
(BoolePoset X) by A4;
id (BoolePoset X) <= closure_op L
by WAYBEL_1:def 14;
then
(id (BoolePoset X)) . F <= (closure_op L) . F
by YELLOW_2:9;
then
F <= (closure_op L) . F
;
then A7:
F c= (closure_op L) . F
by YELLOW_1:2;
(closure_op L) . x in rng (closure_op L)
by A4, FUNCT_1:def 3;
then
(closure_op L) . x in the
carrier of
(Image (closure_op L))
by YELLOW_0:def 15;
then
(closure_op L) . x in the
carrier of
RelStr(# the
carrier of
L, the
InternalRel of
L #)
by WAYBEL10:18;
then A8:
(closure_op L) . x in { Y where Y is Element of L : F c= Y }
by A7;
take
F
;
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E )
F is
compact
by A5, WAYBEL_8:def 1;
hence
F is
finite
by WAYBEL_8:28;
( E = meet { Y where Y is Element of L : F c= Y } & F c= E )
A9:
(uparrow F) /\ the
carrier of
L c= { Y where Y is Element of L : F c= Y }
{ Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the
carrier of
L
then A14:
(uparrow F) /\ the
carrier of
L = { Y where Y is Element of L : F c= Y }
by A9, XBOOLE_0:def 10;
thus A15:
E =
"/\" (
((uparrow F) /\ the carrier of L),
(BoolePoset X))
by A6, WAYBEL10:def 5
.=
meet { Y where Y is Element of L : F c= Y }
by A8, A14, YELLOW_1:20
;
F c= E
hence
F c= E
;
verum
end;
thus
( ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of (CompactSublatt L) )
verumproof
given F being
Element of
(BoolePoset X) such that A17:
F is
finite
and A18:
E = meet { Y where Y is Element of L : F c= Y }
and
F c= E
;
E in the carrier of (CompactSublatt L)
F is
compact
by A17, WAYBEL_8:28;
then A19:
F in [#] (CompactSublatt (BoolePoset X))
by WAYBEL_8:def 1;
A20:
(uparrow F) /\ the
carrier of
L c= { Y where Y is Element of L : F c= Y }
{ Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the
carrier of
L
then A25:
(uparrow F) /\ the
carrier of
L = { Y where Y is Element of L : F c= Y }
by A20, XBOOLE_0:def 10;
id (BoolePoset X) <= closure_op L
by WAYBEL_1:def 14;
then
(id (BoolePoset X)) . F <= (closure_op L) . F
by YELLOW_2:9;
then
F <= (closure_op L) . F
;
then A26:
F c= (closure_op L) . F
by YELLOW_1:2;
F in the
carrier of
(BoolePoset X)
;
then A27:
F in dom (closure_op L)
by FUNCT_2:def 1;
then
(closure_op L) . F in rng (closure_op L)
by FUNCT_1:def 3;
then
(closure_op L) . F in the
carrier of
(Image (closure_op L))
by YELLOW_0:def 15;
then
(closure_op L) . F in the
carrier of
RelStr(# the
carrier of
L, the
InternalRel of
L #)
by WAYBEL10:18;
then
(closure_op L) . F in { Y where Y is Element of L : F c= Y }
by A26;
then E =
"/\" (
((uparrow F) /\ the carrier of L),
(BoolePoset X))
by A18, A25, YELLOW_1:20
.=
(closure_op L) . F
by WAYBEL10:def 5
;
then A28:
E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X)))
by A27, A19, FUNCT_1:def 6;
(closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) =
[#] (CompactSublatt (Image (closure_op L)))
by WAYBEL_8:25
.=
[#] (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #))
by WAYBEL10:18
.=
the
carrier of
(CompactSublatt RelStr(# the carrier of L, the InternalRel of L #))
;
hence
E in the
carrier of
(CompactSublatt L)
by A2, A28, Th5;
verum
end;