let L be LATTICE; ( ex X being non empty 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 non empty 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 non empty 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
; ex X being non empty 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
; 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
; ( c is directed-sups-preserving & L, Image c are_isomorphic )
thus
c is directed-sups-preserving
by A2; 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; verum