let L be LATTICE; :: 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 )

given X being set , p being projection Function of (BoolePoset X),(BoolePoset X) such that A1: p is directed-sups-preserving and

A2: L, Image p are_isomorphic ; :: thesis: L is continuous

Image p is continuous by A1, Th15;

hence L is continuous by A2, Th9, WAYBEL_1:6; :: thesis: verum

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

given X being set , p being projection Function of (BoolePoset X),(BoolePoset X) such that A1: p is directed-sups-preserving and

A2: L, Image p are_isomorphic ; :: thesis: L is continuous

Image p is continuous by A1, Th15;

hence L is continuous by A2, Th9, WAYBEL_1:6; :: thesis: verum