let L be lower-bounded LATTICE; :: thesis: ( L is continuous iff ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) )
thus ( L is continuous implies ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ) :: thesis: ( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous )

proof

assume L is continuous ; :: thesis: ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
then ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) by Lm2;
hence ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ; :: thesis: verum

end;

thus ( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous ) :: thesis: verum

proof

assume ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) ; :: thesis: L is continuous
then ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) by Lm3;
hence L is continuous by Lm4; :: thesis: verum

end;