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 set ; 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 set such that
A3:
y in dom c
and
A4:
y in [#] (CompactSublatt L)
and
A5:
x = c . y
by FUNCT_1:def 12;
A6:
x in rng c
by A3, A5, FUNCT_1:def 5;
then reconsider x' = x as Element of by YELLOW_0:def 15;
reconsider x1 = x' as Element of by A6;
reconsider y' = y as Element of by A3;
y' is compact
by A4, Def1;
then A7:
y' << y'
by WAYBEL_3:def 2;
now
id L <= c
by WAYBEL_1:def 14;
then
(id L) . y' <= c . y'
by YELLOW_2:10;
then A8:
y' <= x1
by A5, TMAP_1:91;
let D be non
empty directed Subset of ;
( x' <= sup D implies ex d being Element of st
( d in D & x' <= d ) )assume A9:
x' <= sup D
;
ex d being Element of st
( d in D & x' <= d )
D c= the
carrier of
(Image c)
;
then A10:
D c= rng c
by YELLOW_0:def 15;
then reconsider D' =
D as non
empty Subset of
by XBOOLE_1:1;
reconsider D' =
D' as non
empty directed Subset of
by YELLOW_2:7;
A11:
ex_sup_of D',
L
by WAYBEL_0:75;
c preserves_sup_of D'
by A1, WAYBEL_0:def 37;
then A12:
c . (sup D') =
sup (c .: D')
by A11, WAYBEL_0:def 31
.=
sup D'
by A2, A10, YELLOW_2:22
;
c . (sup D') = sup D
by A11, WAYBEL_1:58;
then
x1 <= sup D'
by A9, A12, YELLOW_0:60;
then
y' <= sup D'
by A8, ORDERS_2:26;
then consider d' being
Element of
such that A13:
d' in D'
and A14:
y' <= d'
by A7, WAYBEL_3:def 1;
reconsider d =
d' as
Element of
by A13;
take d =
d;
( d in D & x' <= d )thus
d in D
by A13;
x' <= d
d in the
carrier of
(Image c)
;
then
d in rng c
by YELLOW_0:def 15;
then
d' in { z where z is Element of : z = c . z }
by A2, YELLOW_2:21;
then A15:
ex
z' being
Element of st
(
d' = z' &
z' = c . z' )
;
c . y' <= c . d'
by A2, A14, WAYBEL_1:def 2;
hence
x' <= d
by A5, A15, YELLOW_0:61;
verum end;
then
x' << x'
by WAYBEL_3:def 1;
then
x' is compact
by WAYBEL_3:def 2;
hence
x in [#] (CompactSublatt (Image c))
by Def1; verum