let L be lower-bounded LATTICE; :: thesis: ( ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) implies ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) )
given A being lower-bounded algebraic LATTICE, g being Function of A,L such that A1: g is onto and
A2: g is infs-preserving and
A3: g is directed-sups-preserving ; :: thesis: ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
g is upper_adjoint by A2, WAYBEL_1:16;
then consider d being Function of L,A such that
A4: [g,d] is Galois ;
( g is monotone & d is monotone ) by A4, WAYBEL_1:8;
then d * g is monotone by YELLOW_2:12;
then reconsider k = d * g as kernel Function of A,A by A4, WAYBEL_1:41;
d is lower_adjoint by A4;
then A5: k is directed-sups-preserving by A3, Th11;
consider X being non empty set , c being closure Function of (BoolePoset X),(BoolePoset X) such that
A6: c is directed-sups-preserving and
A7: A, Image c are_isomorphic by WAYBEL13:35;
consider f being Function of A,(Image c) such that
A8: f is isomorphic by A7;
reconsider f1 = f " as Function of (Image c),A by A8, WAYBEL_0:67;
reconsider p = ((((inclusion c) * f) * k) * f1) * (corestr c) as Function of (BoolePoset X),(BoolePoset X) ;
A9: f1 * f = id (dom f) by A8, FUNCT_1:39
.= id A by FUNCT_2:def 1 ;
A10: f1 is isomorphic by A8, WAYBEL_0:68;
then rng f1 = the carrier of A by WAYBEL_0:66;
then f1 is onto by FUNCT_2:def 3;
then A11: g * f1 is onto by A1, Lm1;
then (g * f1) * (corestr c) is onto by Lm1;
then A12: rng ((g * f1) * (corestr c)) = the carrier of L by FUNCT_2:def 3
.= dom (((inclusion c) * f) * d) by FUNCT_2:def 1 ;
A13: f is sups-preserving by A8, WAYBEL13:20;
inclusion c is directed-sups-preserving by A6, Th13;
then (inclusion c) * f is directed-sups-preserving by A13, Th11;
then A14: ((inclusion c) * f) * k is directed-sups-preserving by A5, Th11;
take X ; :: thesis: ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
A15: dom (f * d) = the carrier of L by FUNCT_2:def 1;

A16: now :: thesis: for x being object st x in the carrier of L holds
(f * d) . x = (((inclusion c) * f) * d) . x

let x be object ; :: thesis: ( x in the carrier of L implies (f * d) . x = (((inclusion c) * f) * d) . x )
assume A17: x in the carrier of L ; :: thesis: (f * d) . x = (((inclusion c) * f) * d) . x
then (f * d) . x in the carrier of (Image c) by FUNCT_2:5;
hence (f * d) . x = (inclusion c) . ((f * d) . x) by FUNCT_1:18
.= ((inclusion c) * (f * d)) . x by A15, A17, FUNCT_1:13
.= (((inclusion c) * f) * d) . x by RELAT_1:36 ;
:: thesis: verum

end;

A18: ((((inclusion c) * f) * k) * (f1 * (id (Image c)))) * (f * (k * (f1 * (corestr c)))) = ((((inclusion c) * f) * k) * f1) * (f * (k * (f1 * (corestr c)))) by FUNCT_2:17
.= (((((inclusion c) * f) * k) * f1) * f) * (k * (f1 * (corestr c))) by RELAT_1:36
.= ((((inclusion c) * f) * k) * (id A)) * (k * (f1 * (corestr c))) by A9, RELAT_1:36
.= (((inclusion c) * f) * k) * (k * (f1 * (corestr c))) by FUNCT_2:17
.= ((((inclusion c) * f) * k) * k) * (f1 * (corestr c)) by RELAT_1:36
.= (((inclusion c) * f) * (k * k)) * (f1 * (corestr c)) by RELAT_1:36
.= (((inclusion c) * f) * k) * (f1 * (corestr c)) by QUANTAL1:def 9
.= p by RELAT_1:36 ;
p * p = (((((inclusion c) * f) * k) * f1) * (corestr c)) * ((((inclusion c) * f) * k) * (f1 * (corestr c))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * (corestr c)) * (((inclusion c) * f) * (k * (f1 * (corestr c)))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * (corestr c)) * ((inclusion c) * (f * (k * (f1 * (corestr c))))) by RELAT_1:36
.= ((((((inclusion c) * f) * k) * f1) * (corestr c)) * (inclusion c)) * (f * (k * (f1 * (corestr c)))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * ((corestr c) * (inclusion c))) * (f * (k * (f1 * (corestr c)))) by RELAT_1:36
.= (((((inclusion c) * f) * k) * f1) * (id (Image c))) * (f * (k * (f1 * (corestr c)))) by WAYBEL_1:33
.= p by A18, RELAT_1:36 ;
then A19: p is idempotent by QUANTAL1:def 9;
(inclusion c) * f is monotone by A8, YELLOW_2:12;
then ((inclusion c) * f) * k is monotone by YELLOW_2:12;
then (((inclusion c) * f) * k) * f1 is monotone by A10, YELLOW_2:12;
then p is monotone by YELLOW_2:12;
then reconsider p = p as projection Function of (BoolePoset X),(BoolePoset X) by A19, WAYBEL_1:def 13;
take p ; :: thesis: ( p is directed-sups-preserving & L, Image p are_isomorphic )
p = (((((inclusion c) * f) * d) * g) * f1) * (corestr c) by RELAT_1:36
.= ((((inclusion c) * f) * d) * g) * (f1 * (corestr c)) by RELAT_1:36
.= (((inclusion c) * f) * d) * (g * (f1 * (corestr c))) by RELAT_1:36
.= (((inclusion c) * f) * d) * ((g * f1) * (corestr c)) by RELAT_1:36 ;
then A20: rng (((inclusion c) * f) * d) = rng p by A12, RELAT_1:28;
dom (((inclusion c) * f) * d) = the carrier of L by FUNCT_2:def 1;
then rng (f * d) = rng (((inclusion c) * f) * d) by A15, A16, FUNCT_1:2;
then A21: the carrier of (subrelstr (rng (f * d))) = rng (((inclusion c) * f) * d) by YELLOW_0:def 15;
[f1,f] is Galois by A8, Th6;
then [(g * f1),(f * d)] is Galois by A4, Th5;
then A22: L, Image (f * d) are_isomorphic by A11, Th4;
f1 is sups-preserving by A10, WAYBEL13:20;
then ( corestr c is sups-preserving & (((inclusion c) * f) * k) * f1 is directed-sups-preserving ) by A14, Th11, WAYBEL_1:55;
hence p is directed-sups-preserving by Th11; :: thesis: L, Image p are_isomorphic
subrelstr (rng (f * d)) is strict full SubRelStr of BoolePoset X by Th1;
hence L, Image p are_isomorphic by A22, A21, A20, YELLOW_0:def 15; :: thesis: verum