let L be LATTICE; :: thesis: ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies 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 ) )
given X being set , S being full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and
A2: S is directed-sups-inheriting and
A3: L,S are_isomorphic ; :: 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 )
reconsider S9 = S as closure System of BoolePoset X by A1;
take X ; :: thesis: ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
reconsider c = closure_op S9 as closure Function of (BoolePoset X),(BoolePoset X) ;
take c ; :: thesis: ( c is directed-sups-preserving & L, Image c are_isomorphic )
thus c is directed-sups-preserving by A2; :: thesis: L, Image c are_isomorphic
Image c = RelStr(# the carrier of S, the InternalRel of S #) by WAYBEL10:18;
then S, Image c are_isomorphic by Th26;
hence L, Image c are_isomorphic by A3, WAYBEL_1:7; :: thesis: verum