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 (),() 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 (),() st
( p is directed-sups-preserving & L, Image p are_isomorphic )

g is upper_adjoint by ;
then consider d being Function of L,A such that
A4: [g,d] is Galois ;
( g is monotone & d is monotone ) by ;
then d * g is monotone by YELLOW_2:12;
then reconsider k = d * g as kernel Function of A,A by ;
d is lower_adjoint by A4;
then A5: k is directed-sups-preserving by ;
consider X being non empty set , c being closure Function of (),() such that
A6: c is directed-sups-preserving and
A7: A, Image c are_isomorphic by WAYBEL13:35;
consider f being Function of A,() such that
A8: f is isomorphic by A7;
reconsider f1 = f " as Function of (),A by ;
reconsider p = (((() * f) * k) * f1) * () as Function of (),() ;
A9: f1 * f = id (dom f) by
.= id A by FUNCT_2:def 1 ;
A10: f1 is isomorphic by ;
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 ;
then (g * f1) * () is onto by Lm1;
then A12: rng ((g * f1) * ()) = the carrier of L by FUNCT_2:def 3
.= dom ((() * f) * d) by FUNCT_2:def 1 ;
A13: f is sups-preserving by ;
inclusion c is directed-sups-preserving by ;
then (inclusion c) * f is directed-sups-preserving by ;
then A14: ((inclusion c) * f) * k is directed-sups-preserving by ;
take X ; :: thesis: ex p being projection Function of (),() 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 = ((() * f) * d) . x
let x be object ; :: thesis: ( x in the carrier of L implies (f * d) . x = ((() * f) * d) . x )
assume A17: x in the carrier of L ; :: thesis: (f * d) . x = ((() * f) * d) . x
then (f * d) . x in the carrier of () by FUNCT_2:5;
hence (f * d) . x = () . ((f * d) . x) by FUNCT_1:18
.= (() * (f * d)) . x by
.= ((() * f) * d) . x by RELAT_1:36 ;
:: thesis: verum
end;
A18: (((() * f) * k) * (f1 * (id ()))) * (f * (k * (f1 * ()))) = (((() * f) * k) * f1) * (f * (k * (f1 * ()))) by FUNCT_2:17
.= ((((() * f) * k) * f1) * f) * (k * (f1 * ())) by RELAT_1:36
.= (((() * f) * k) * (id A)) * (k * (f1 * ())) by
.= ((() * f) * k) * (k * (f1 * ())) by FUNCT_2:17
.= (((() * f) * k) * k) * (f1 * ()) by RELAT_1:36
.= ((() * f) * (k * k)) * (f1 * ()) by RELAT_1:36
.= ((() * f) * k) * (f1 * ()) by QUANTAL1:def 9
.= p by RELAT_1:36 ;
p * p = ((((() * f) * k) * f1) * ()) * (((() * f) * k) * (f1 * ())) by RELAT_1:36
.= ((((() * f) * k) * f1) * ()) * ((() * f) * (k * (f1 * ()))) by RELAT_1:36
.= ((((() * f) * k) * f1) * ()) * (() * (f * (k * (f1 * ())))) by RELAT_1:36
.= (((((() * f) * k) * f1) * ()) * ()) * (f * (k * (f1 * ()))) by RELAT_1:36
.= ((((() * f) * k) * f1) * (() * ())) * (f * (k * (f1 * ()))) by RELAT_1:36
.= ((((() * f) * k) * f1) * (id ())) * (f * (k * (f1 * ()))) by WAYBEL_1:33
.= p by ;
then A19: p is idempotent by QUANTAL1:def 9;
(inclusion c) * f is monotone by ;
then ((inclusion c) * f) * k is monotone by YELLOW_2:12;
then (((inclusion c) * f) * k) * f1 is monotone by ;
then p is monotone by YELLOW_2:12;
then reconsider p = p as projection Function of (),() by ;
take p ; :: thesis:
p = ((((() * f) * d) * g) * f1) * () by RELAT_1:36
.= (((() * f) * d) * g) * (f1 * ()) by RELAT_1:36
.= ((() * f) * d) * (g * (f1 * ())) by RELAT_1:36
.= ((() * f) * d) * ((g * f1) * ()) by RELAT_1:36 ;
then A20: rng ((() * f) * d) = rng p by ;
dom ((() * f) * d) = the carrier of L by FUNCT_2:def 1;
then rng (f * d) = rng ((() * f) * d) by ;
then A21: the carrier of (subrelstr (rng (f * d))) = rng ((() * f) * d) by YELLOW_0:def 15;
[f1,f] is Galois by ;
then [(g * f1),(f * d)] is Galois by ;
then A22: L, Image (f * d) are_isomorphic by ;
f1 is sups-preserving by ;
then ( corestr c is sups-preserving & ((() * f) * k) * f1 is directed-sups-preserving ) by ;
hence p is directed-sups-preserving by Th11; :: thesis:
subrelstr (rng (f * d)) is strict full SubRelStr of BoolePoset X by Th1;
hence L, Image p are_isomorphic by ; :: thesis: verum