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

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 A5;
then g . x c= g . y by A5;
then g . x <= g . y by YELLOW_1:2;
hence g1 . x <= g1 . y by YELLOW_0:60; :: thesis:

end;

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

assume g1 . x <= g1 . y ; :: thesis:
then g . x <= g . y by YELLOW_0:59;
then g . x c= g . y by YELLOW_1:2;
then g . x c= compactbelow y by A5;
then A8: compactbelow x c= compactbelow y by A5;
( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by A6, YELLOW_0:17;
then sup (compactbelow x) <= sup (compactbelow y) by A8, YELLOW_0:34;
then x <= sup (compactbelow y) by A1, WAYBEL_8:def 3;
hence x <= y by A1, WAYBEL_8:def 3; :: thesis:

end;

end;

then A9: g1 is isomorphic by A4, A7, WAYBEL_0:66;
then reconsider f1 = g1 " as Function of S,L by WAYBEL_0:67;
A10: f1 is isomorphic by A9, WAYBEL_0:68;

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

let X2 be finite Subset of (f1 .: Y); :: thesis:
A12: g1 " (g1 .: X2) c= X2 by A4, FUNCT_1:82;

let v be object ; :: thesis:
assume v in g1 .: X2 ; :: thesis:
then ex u being object st
( u in dom g1 & u in X2 & v = g1 . u ) by FUNCT_1:def 6;
then v in g1 .: (f1 .: Y) by FUNCT_1:def 6;
then v in g1 .: (g1 " Y) by A4, FUNCT_1:85;
hence v in Y by A7, FUNCT_1:77; :: thesis:

end;

then reconsider Y1 = g1 .: X2 as finite Subset of Y by TARSKI:def 3;
consider y1 being Element of S such that
A13: y1 in Y and
A14: y1 is_>=_than Y1 by A11, WAYBEL_0:1;
take f1y1 = f1 . y1; :: thesis:
y1 in the carrier of S ;
then y1 in dom f1 by FUNCT_2:def 1;
hence f1y1 in f1 .: Y by A13, FUNCT_1:def 6; :: thesis:
X2 c= the carrier of L by XBOOLE_1:1;
then X2 c= dom g1 by FUNCT_2:def 1;
then A15: X2 c= g1 " (g1 .: X2) by FUNCT_1:76;
f1 .: Y1 = g1 " (g1 .: X2) by A4, FUNCT_1:85
.= X2 by A15, A12, XBOOLE_0:def 10 ;
hence f1y1 is_>=_than X2 by A10, A14, Th19; :: thesis:

end;

then reconsider X1 = f1 .: Y as non empty directed Subset of L by WAYBEL_0:1;
sup X1 in the carrier of L ;
then sup X1 in dom g by FUNCT_2:def 1;
then A16: g . (sup X1) in rng g by FUNCT_1:def 3;
( ex_sup_of X1,L & g preserves_sup_of X1 ) by A6, A3, WAYBEL_0:def 37, YELLOW_0:17;
then A17: sup (g .: X1) in rng g by A16, WAYBEL_0:def 31;
g .: X1 = g .: (g1 " Y) by A4, FUNCT_1:85
.= Y by A7, FUNCT_1:77 ;
hence "\/" (Y,(BoolePoset X)) in the carrier of S by A17, YELLOW_0:def 15; :: thesis:

end;

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