let L be lower-bounded LATTICE; :: thesis: ( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) )

hereby :: thesis: ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic )

assume L is algebraic ; :: thesis: ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
then 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 ) by Lm1;
hence ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) by Lm2; :: thesis: verum

end;

thus ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) by Lm5; :: thesis: verum