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 )

( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies L is continuous ) :: thesis: verum

( 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

thus
( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
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;( 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

( 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;( 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