let L be algebraic LATTICE; for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let c be closure Function of L,L; ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) )
assume A1:
c is directed-sups-preserving
; c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let x be object ; TARSKI:def 3 ( not x in c .: ([#] (CompactSublatt L)) or x in [#] (CompactSublatt (Image c)) )
A2:
( c is idempotent & c is monotone )
by WAYBEL_1:def 13;
assume
x in c .: ([#] (CompactSublatt L))
; x in [#] (CompactSublatt (Image c))
then consider y being object such that
A3:
y in dom c
and
A4:
y in [#] (CompactSublatt L)
and
A5:
x = c . y
by FUNCT_1:def 6;
A6:
x in rng c
by A3, A5, FUNCT_1:def 3;
then reconsider x9 = x as Element of (Image c) by YELLOW_0:def 15;
reconsider x1 = x9 as Element of L by A6;
reconsider y9 = y as Element of L by A3;
y9 is compact
by A4, Def1;
then A7:
y9 << y9
by WAYBEL_3:def 2;
now for D being non empty directed Subset of (Image c) st x9 <= sup D holds
ex d being Element of (Image c) st
( d in D & x9 <= d )
id L <= c
by WAYBEL_1:def 14;
then
(id L) . y9 <= c . y9
by YELLOW_2:9;
then A8:
y9 <= x1
by A5, FUNCT_1:18;
let D be non
empty directed Subset of
(Image c);
( x9 <= sup D implies ex d being Element of (Image c) st
( d in D & x9 <= d ) )assume A9:
x9 <= sup D
;
ex d being Element of (Image c) st
( d in D & x9 <= d )
D c= the
carrier of
(Image c)
;
then A10:
D c= rng c
by YELLOW_0:def 15;
then reconsider D9 =
D as non
empty Subset of
L by XBOOLE_1:1;
reconsider D9 =
D9 as non
empty directed Subset of
L by YELLOW_2:7;
A11:
ex_sup_of D9,
L
by WAYBEL_0:75;
c preserves_sup_of D9
by A1, WAYBEL_0:def 37;
then A12:
c . (sup D9) =
sup (c .: D9)
by A11, WAYBEL_0:def 31
.=
sup D9
by A2, A10, YELLOW_2:20
;
c . (sup D9) = sup D
by A11, WAYBEL_1:55;
then
x1 <= sup D9
by A9, A12, YELLOW_0:59;
then
y9 <= sup D9
by A8, ORDERS_2:3;
then consider d9 being
Element of
L such that A13:
d9 in D9
and A14:
y9 <= d9
by A7, WAYBEL_3:def 1;
reconsider d =
d9 as
Element of
(Image c) by A13;
take d =
d;
( d in D & x9 <= d )thus
d in D
by A13;
x9 <= d
d in the
carrier of
(Image c)
;
then
d in rng c
by YELLOW_0:def 15;
then
d9 in { z where z is Element of L : z = c . z }
by A2, YELLOW_2:19;
then A15:
ex
z9 being
Element of
L st
(
d9 = z9 &
z9 = c . z9 )
;
c . y9 <= c . d9
by A2, A14, WAYBEL_1:def 2;
hence
x9 <= d
by A5, A15, YELLOW_0:60;
verum end;
then
x9 << x9
by WAYBEL_3:def 1;
then
x9 is compact
by WAYBEL_3:def 2;
hence
x in [#] (CompactSublatt (Image c))
by Def1; verum