let X, E be set ; :: thesis: 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; :: thesis: ( 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:
L is complete LATTICE
by YELLOW_2:32;
A2:
the carrier of L c= the carrier of (BoolePoset X)
by YELLOW_0:def 13;
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 ) )
:: thesis: ( 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
assume A3:
E in the
carrier of
(CompactSublatt L)
;
:: thesis: 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 )
(closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) =
[#] (CompactSublatt (Image (closure_op L)))
by WAYBEL_8:27
.=
[#] (CompactSublatt RelStr(# the carrier of L,the InternalRel of L #))
by WAYBEL10:19
.=
the
carrier of
(CompactSublatt RelStr(# the carrier of L,the InternalRel of L #))
;
then
E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X)))
by A1, A3, Th5;
then consider x being
set 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 12;
reconsider F =
x as
Element of
(BoolePoset X) by A4;
take
F
;
:: thesis: ( 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:30;
:: thesis: ( E = meet { Y where Y is Element of L : F c= Y } & F c= E )
(closure_op L) . x in rng (closure_op L)
by A4, FUNCT_1:def 5;
then
(closure_op L) . x in the
carrier of
(Image (closure_op L))
by YELLOW_0:def 15;
then A7:
(closure_op L) . x in the
carrier of
RelStr(# the
carrier of
L,the
InternalRel of
L #)
by WAYBEL10:19;
id (BoolePoset X) <= closure_op L
by WAYBEL_1:def 14;
then
(id (BoolePoset X)) . F <= (closure_op L) . F
by YELLOW_2:10;
then
F <= (closure_op L) . F
by TMAP_1:91;
then
F c= (closure_op L) . F
by YELLOW_1:2;
then A8:
(closure_op L) . x in { Y where Y is Element of L : F c= Y }
by A7;
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 6
.=
meet { Y where Y is Element of L : F c= Y }
by A8, A14, YELLOW_1:20
;
:: thesis: F c= E
hence
F c= E
by TARSKI:def 3;
:: thesis: 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) )
:: thesis: verumproof
given F being
Element of
(BoolePoset X) such that A19:
F is
finite
and A20:
E = meet { Y where Y is Element of L : F c= Y }
and
F c= E
;
:: thesis: E in the carrier of (CompactSublatt L)
F in the
carrier of
(BoolePoset X)
;
then A21:
F in dom (closure_op L)
by FUNCT_2:def 1;
F is
compact
by A19, WAYBEL_8:30;
then
F in the
carrier of
(CompactSublatt (BoolePoset X))
by WAYBEL_8:def 1;
then A22:
F in [#] (CompactSublatt (BoolePoset X))
;
(closure_op L) . F in rng (closure_op L)
by A21, FUNCT_1:def 5;
then
(closure_op L) . F in the
carrier of
(Image (closure_op L))
by YELLOW_0:def 15;
then A23:
(closure_op L) . F in the
carrier of
RelStr(# the
carrier of
L,the
InternalRel of
L #)
by WAYBEL10:19;
id (BoolePoset X) <= closure_op L
by WAYBEL_1:def 14;
then
(id (BoolePoset X)) . F <= (closure_op L) . F
by YELLOW_2:10;
then
F <= (closure_op L) . F
by TMAP_1:91;
then
F c= (closure_op L) . F
by YELLOW_1:2;
then A24:
(closure_op L) . F in { Y where Y is Element of L : F c= Y }
by A23;
A25:
(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
(uparrow F) /\ the
carrier of
L = { Y where Y is Element of L : F c= Y }
by A25, XBOOLE_0:def 10;
then E =
"/\" ((uparrow F) /\ the carrier of L),
(BoolePoset X)
by A20, A24, YELLOW_1:20
.=
(closure_op L) . F
by WAYBEL10:def 6
;
then A30:
E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X)))
by A21, A22, FUNCT_1:def 12;
(closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) =
[#] (CompactSublatt (Image (closure_op L)))
by WAYBEL_8:27
.=
[#] (CompactSublatt RelStr(# the carrier of L,the InternalRel of L #))
by WAYBEL10:19
.=
the
carrier of
(CompactSublatt RelStr(# the carrier of L,the InternalRel of L #))
;
hence
E in the
carrier of
(CompactSublatt L)
by A1, A30, Th5;
:: thesis: verum
end;