let L be lower-bounded LATTICE; :: thesis: ( ( L is continuous implies 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 ) ) & ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )

thus ( L is continuous implies 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 ) ) :: thesis: ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous )

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) by Lm4; :: thesis: verum

( p is directed-sups-preserving & L, Image p are_isomorphic ) ) & ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) )

thus ( L is continuous implies 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 ) ) :: thesis: ( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous )

proof

thus
( ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
assume
L is continuous
; :: thesis: 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 )

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

end;( p is directed-sups-preserving & L, Image p are_isomorphic )

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

( p is directed-sups-preserving & L, Image p are_isomorphic ) implies L is continuous ) by Lm4; :: thesis: verum