let L be LATTICE; :: thesis: ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic )
given X being set , c being closure Function of (BoolePoset X),(BoolePoset X) such that A1: c is directed-sups-preserving and
A2: L, Image c are_isomorphic ; :: thesis: L is algebraic
A3: Image c is complete LATTICE by A1, YELLOW_2:37;
Image c is algebraic LATTICE by A1, WAYBEL_8:26;
hence L is algebraic by A2, A3, Th32, WAYBEL_1:7; :: thesis: verum