let L be lower-bounded algebraic LATTICE; :: thesis: ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g is infs-preserving & g is directed-sups-preserving & g is one-to-one & ( for x being Element of L holds g . x = compactbelow x ) )
deffunc H₁( Element of L) -> Element of bool the carrier of L = compactbelow $1;
A1: for y being Element of L holds H₁(y) is Element of (InclPoset (Ids (CompactSublatt L)))

proof

let y be Element of L; :: thesis: H₁(y) is Element of (InclPoset (Ids (CompactSublatt L)))
reconsider comy = compactbelow y as non empty directed Subset of L by WAYBEL_8:def 4;
reconsider comy = comy as non empty Subset of (CompactSublatt L) by Th2;
reconsider comy = comy as non empty directed Subset of (CompactSublatt L) by WAYBEL10:24;

now

let x1, z1 be Element of (CompactSublatt L); :: thesis: ( x1 in comy & z1 <= x1 implies z1 in comy )
reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0:59;
assume A2: ( x1 in comy & z1 <= x1 ) ; :: thesis: z1 in comy
then A3: ( x2 <= y & x2 is compact ) by WAYBEL_8:4;
z2 <= x2 by A2, YELLOW_0:60;
then A4: z2 <= y by A3, ORDERS_2:26;
z2 is compact by WAYBEL_8:def 1;
hence z1 in comy by A4, WAYBEL_8:4; :: thesis: verum

end;

then comy is lower by WAYBEL_0:def 19;
hence H₁(y) is Element of (InclPoset (Ids (CompactSublatt L))) by YELLOW_2:43; :: thesis: verum

end;

consider g1 being Function of L,(InclPoset (Ids (CompactSublatt L))) such that
A5: for y being Element of L holds g1 . y = H₁(y) from FUNCT_2:sch 9(A1);

now

let k be set ; :: thesis: ( k in the carrier of (InclPoset (Ids (CompactSublatt L))) implies k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) )
assume k in the carrier of (InclPoset (Ids (CompactSublatt L))) ; :: thesis: k in the carrier of (BoolePoset the carrier of (CompactSublatt L))
then k is Ideal of (CompactSublatt L) by YELLOW_2:43;
then k is Element of (BoolePoset the carrier of (CompactSublatt L)) by WAYBEL_8:28;
hence k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) ; :: thesis: verum

end;

then the carrier of (InclPoset (Ids (CompactSublatt L))) c= the carrier of (BoolePoset the carrier of (CompactSublatt L)) by TARSKI:def 3;
then reconsider g = g1 as Function of L,(BoolePoset the carrier of (CompactSublatt L)) by FUNCT_2:9;
take g ; :: thesis: ( g is infs-preserving & g is directed-sups-preserving & g is one-to-one & ( for x being Element of L holds g . x = compactbelow x ) )
A6: g1 is isomorphic by A5, Th16;
then A7: ( g1 is infs-preserving & g1 is sups-preserving ) ;
then A8: ( g1 is infs-preserving & g1 is directed-sups-preserving ) ;
A9: InclPoset (Ids (CompactSublatt L)) is full infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of (CompactSublatt L) by Th23;
then consider g2 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) such that
A10: g1 = g2 and
A11: g2 is infs-preserving by A7, Th21;
thus g is infs-preserving by A10, A11; :: thesis: ( g is directed-sups-preserving & g is one-to-one & ( for x being Element of L holds g . x = compactbelow x ) )
g1 is monotone by A6;
then consider g3 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) such that
A12: g1 = g3 and
A13: g3 is directed-sups-preserving by A8, A9, Th22;
thus g is directed-sups-preserving by A12, A13; :: thesis: ( g is one-to-one & ( for x being Element of L holds g . x = compactbelow x ) )
for x1, x2 being set st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2 by A6, FUNCT_1:def 8;
hence g is one-to-one by FUNCT_1:def 8; :: thesis: for x being Element of L holds g . x = compactbelow x
let x be Element of L; :: thesis: g . x = compactbelow x
thus g . x = compactbelow x by A5; :: thesis: verum