theorem :: WAYBEL15:18

for L being lower-bounded LATTICE holds
( ( 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 ) )