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