let L be lower-bounded LATTICE; :: thesis:
assume A1: L is algebraic ; :: thesis:
then reconsider L' = L as lower-bounded algebraic LATTICE ;
A2: L' is complete ;
consider g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) such that
A3: g is infs-preserving and
A4: g is directed-sups-preserving and
A5: g is one-to-one and
A6: for x being Element of L holds g . x = compactbelow x by A1, Th24;
take X = the carrier of (CompactSublatt L); :: thesis:
reconsider S = Image g as non empty full SubRelStr of BoolePoset X ;
take S ; :: thesis:
A7: dom g = the carrier of L by FUNCT_2:def 1;
A8: rng g = the carrier of S by YELLOW_0:def 15;
then reconsider g1 = g as Function of L,S by A7, FUNCT_2:3;

let x, y be Element of L; :: thesis:
thus ( x <= y implies g1 . x <= g1 . y ) :: thesis:

assume x <= y ; :: thesis:
then compactbelow x c= compactbelow y by Th1;
then g . x c= compactbelow y by A6;
then g . x c= g . y by A6;
then g . x <= g . y by YELLOW_1:2;
hence g1 . x <= g1 . y by YELLOW_0:61; :: thesis:

end;

thus ( g1 . x <= g1 . y implies x <= y ) :: thesis:

A9: L is satisfying_axiom_K by A1;
A10: ( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by A2, YELLOW_0:17;
assume g1 . x <= g1 . y ; :: thesis:
then g . x <= g . y by YELLOW_0:60;
then g . x c= g . y by YELLOW_1:2;
then g . x c= compactbelow y by A6;
then compactbelow x c= compactbelow y by A6;
then sup (compactbelow x) <= sup (compactbelow y) by A10, YELLOW_0:34;
then x <= sup (compactbelow y) by A9, WAYBEL_8:def 3;
hence x <= y by A9, WAYBEL_8:def 3; :: thesis:

end;

then A11: g1 is isomorphic by A5, A8, WAYBEL_0:66;
then reconsider f1 = g1 " as Function of S,L by WAYBEL_0:67;
A12: f1 is isomorphic by A11, WAYBEL_0:68;
thus S is infs-inheriting by A2, A3, YELLOW_2:35; :: thesis:

let Y be directed Subset of S; :: thesis:
assume that
A13: Y <> {} and
ex_sup_of Y, BoolePoset X ; :: thesis:

let X2 be finite Subset of (f1 .: Y); :: thesis:

let v be set ; :: thesis:
assume v in g1 .: X2 ; :: thesis:
then consider u being set such that
A14: u in dom g1 and
A15: u in X2 and
A16: v = g1 . u by FUNCT_1:def 12;
v in g1 .: (f1 .: Y) by A14, A15, A16, FUNCT_1:def 12;
then v in g1 .: (g1 " Y) by A5, FUNCT_1:155;
hence v in Y by A8, FUNCT_1:147; :: thesis:

end;

then reconsider Y1 = g1 .: X2 as finite Subset of Y by TARSKI:def 3;
consider y1 being Element of S such that
A17: y1 in Y and
A18: y1 is_>=_than Y1 by A13, WAYBEL_0:1;
take f1y1 = f1 . y1; :: thesis:
( not the carrier of L is empty & y1 in the carrier of S ) ;
then y1 in dom f1 by FUNCT_2:def 1;
hence f1y1 in f1 .: Y by A17, FUNCT_1:def 12; :: thesis:
( X2 c= the carrier of L & not the carrier of S is empty ) by XBOOLE_1:1;
then X2 c= dom g1 by FUNCT_2:def 1;
then A19: X2 c= g1 " (g1 .: X2) by FUNCT_1:146;
A20: g1 " (g1 .: X2) c= X2 by A5, FUNCT_1:152;
f1 .: Y1 = g1 " (g1 .: X2) by A5, FUNCT_1:155
.= X2 by A19, A20, XBOOLE_0:def 10 ;
hence f1y1 is_>=_than X2 by A12, A18, Th19; :: thesis:

end;

then reconsider X1 = f1 .: Y as non empty directed Subset of L by WAYBEL_0:1;
A21: g .: X1 = g .: (g1 " Y) by A5, FUNCT_1:155
.= Y by A8, FUNCT_1:147 ;
A22: ex_sup_of X1,L by A2, YELLOW_0:17;
A23: g preserves_sup_of X1 by A4, WAYBEL_0:def 37;
( sup X1 in the carrier of L & not the carrier of (BoolePoset X) is empty ) ;
then sup X1 in dom g by FUNCT_2:def 1;
then g . (sup X1) in rng g by FUNCT_1:def 5;
then sup (g .: X1) in rng g by A22, A23, WAYBEL_0:def 31;
hence "\/" Y,(BoolePoset X) in the carrier of S by A21, YELLOW_0:def 15; :: thesis:

end;

hence S is directed-sups-inheriting by WAYBEL_0:def 4; :: thesis:
thus L,S are_isomorphic by A11, WAYBEL_1:def 8; :: thesis: