let L be lower-bounded LATTICE; :: thesis: ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) )
assume A1: L is algebraic ; :: thesis: ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
then reconsider L9 = L as lower-bounded algebraic LATTICE ;
take X = the carrier of (CompactSublatt L); :: thesis: ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
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 one-to-one 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: ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
A6: L9 is complete ;
hence S is infs-inheriting by A2, YELLOW_2:33; :: thesis: ( S is directed-sups-inheriting & L,S are_isomorphic )
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;

now :: thesis: for x, y being Element of L holds
( ( x <= y implies g1 . x <= g1 . y ) & ( g1 . x <= g1 . y implies x <= y ) )

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

proof

assume x <= y ; :: thesis: g1 . x <= g1 . y
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: verum

end;

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

proof

assume g1 . x <= g1 . y ; :: thesis: x <= y
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: verum

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;

now :: thesis: for Y being directed Subset of S st Y <> {} & ex_sup_of Y, BoolePoset X holds
"\/" (Y,(BoolePoset X)) in the carrier of S

let Y be directed Subset of S; :: thesis: ( Y <> {} & ex_sup_of Y, BoolePoset X implies "\/" (Y,(BoolePoset X)) in the carrier of S )
assume that
A11: Y <> {} and
ex_sup_of Y, BoolePoset X ; :: thesis: "\/" (Y,(BoolePoset X)) in the carrier of S

now :: thesis: for X2 being finite Subset of (f1 .: Y) ex f1y1 being Element of the carrier of L st
( f1y1 in f1 .: Y & f1y1 is_>=_than X2 )

let X2 be finite Subset of (f1 .: Y); :: thesis: ex f1y1 being Element of the carrier of L st
( f1y1 in f1 .: Y & f1y1 is_>=_than X2 )
A12: g1 " (g1 .: X2) c= X2 by A4, FUNCT_1:82;

now :: thesis: for v being object st v in g1 .: X2 holds
v in Y

let v be object ; :: thesis: ( v in g1 .: X2 implies v in Y )
assume v in g1 .: X2 ; :: thesis: v in Y
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: verum

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: ( f1y1 in f1 .: Y & f1y1 is_>=_than X2 )
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: f1y1 is_>=_than X2
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: verum

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: verum

end;

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