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 )
consider X being non empty set , c being closure Function of (BoolePoset X),(BoolePoset X) such that
A4: c is directed-sups-preserving and
A5: A, Image c are_isomorphic by WAYBEL13:35;
consider f being Function of A,(Image c) such that
A6: f is isomorphic by A5, WAYBEL_1:def 8;
reconsider f1 = f " as Function of (Image c),A by A6, WAYBEL_0:67;
A8: f1 is isomorphic by A6, WAYBEL_0:68;
g is upper_adjoint by A2, WAYBEL_1:17;
then consider d being Function of L,A such that
A9: [g,d] is Galois by WAYBEL_1:def 11;
( g is monotone & d is monotone ) by A9, WAYBEL_1:9;
then d * g is monotone by YELLOW_2:14;
then reconsider k = d * g as kernel Function of A,A by A9, WAYBEL_1:44;
d is lower_adjoint by A9, WAYBEL_1:10;
then A10: k is directed-sups-preserving by A3, Th13;
A11: f1 * f = id (dom f) by A6, FUNCT_1:61
.= id A by FUNCT_2:def 1 ;
reconsider p = ((((inclusion c) * f) * k) * f1) * (corestr c) as Function of (BoolePoset X),(BoolePoset X) ;
A12: ((((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:23
.= (((((inclusion c) * f) * k) * f1) * f) * (k * (f1 * (corestr c))) by RELAT_1:55
.= ((((inclusion c) * f) * k) * (id A)) * (k * (f1 * (corestr c))) by A11, RELAT_1:55
.= (((inclusion c) * f) * k) * (k * (f1 * (corestr c))) by FUNCT_2:23
.= ((((inclusion c) * f) * k) * k) * (f1 * (corestr c)) by RELAT_1:55
.= (((inclusion c) * f) * (k * k)) * (f1 * (corestr c)) by RELAT_1:55
.= (((inclusion c) * f) * k) * (f1 * (corestr c)) by QUANTAL1:def 9
.= p by RELAT_1:55 ;
p * p = (((((inclusion c) * f) * k) * f1) * (corestr c)) * ((((inclusion c) * f) * k) * (f1 * (corestr c))) by RELAT_1:55
.= (((((inclusion c) * f) * k) * f1) * (corestr c)) * (((inclusion c) * f) * (k * (f1 * (corestr c)))) by RELAT_1:55
.= (((((inclusion c) * f) * k) * f1) * (corestr c)) * ((inclusion c) * (f * (k * (f1 * (corestr c))))) by RELAT_1:55
.= ((((((inclusion c) * f) * k) * f1) * (corestr c)) * (inclusion c)) * (f * (k * (f1 * (corestr c)))) by RELAT_1:55
.= (((((inclusion c) * f) * k) * f1) * ((corestr c) * (inclusion c))) * (f * (k * (f1 * (corestr c)))) by RELAT_1:55
.= (((((inclusion c) * f) * k) * f1) * (id (Image c))) * (f * (k * (f1 * (corestr c)))) by WAYBEL_1:36
.= p by A12, RELAT_1:55 ;
then A13: p is idempotent by QUANTAL1:def 9;
(inclusion c) * f is monotone by A6, YELLOW_2:14;
then ((inclusion c) * f) * k is monotone by YELLOW_2:14;
then (((inclusion c) * f) * k) * f1 is monotone by A8, YELLOW_2:14;
then p is monotone by YELLOW_2:14;
then reconsider p = p as projection Function of (BoolePoset X),(BoolePoset X) by A13, WAYBEL_1:def 13;
take X ; :: thesis: ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
take p ; :: thesis: ( p is directed-sups-preserving & L, Image p are_isomorphic )
A16: inclusion c is directed-sups-preserving by A4, Th15;
B17: f is sups-preserving by A6, WAYBEL13:20;
B18: f1 is sups-preserving by A8, WAYBEL13:20;
B19: corestr c is sups-preserving by WAYBEL_1:58;
(inclusion c) * f is directed-sups-preserving by A16, B17, Th13;
then ((inclusion c) * f) * k is directed-sups-preserving by A10, Th13;
then (((inclusion c) * f) * k) * f1 is directed-sups-preserving by B18, Th13;
hence p is directed-sups-preserving by B19, Th13; :: thesis: L, Image p are_isomorphic
rng f1 = the carrier of A by A8, WAYBEL_0:66;
then f1 is onto by FUNCT_2:def 3;
then A20: g * f1 is onto by A1, Th2;
then A21: (g * f1) * (corestr c) is onto by Th2;
[f1,f] is Galois by A6, Th8;
then [(g * f1),(f * d)] is Galois by A9, Th7;
then A22: L, Image (f * d) are_isomorphic by A20, Th6;
A23: dom (f * d) = the carrier of L by FUNCT_2:def 1;
A24: dom (((inclusion c) * f) * d) = the carrier of L by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier of L implies (f * d) . x = (((inclusion c) * f) * d) . x )
assume A25: 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:7;
hence (f * d) . x = (inclusion c) . ((f * d) . x) by TMAP_1:91
.= ((inclusion c) * (f * d)) . x by A23, A25, FUNCT_1:23
.= (((inclusion c) * f) * d) . x by RELAT_1:55 ;
:: thesis: verum

end;

then rng (f * d) = rng (((inclusion c) * f) * d) by A23, A24, FUNCT_1:9;
then A26: the carrier of (subrelstr (rng (f * d))) = rng (((inclusion c) * f) * d) by YELLOW_0:def 15;
A27: subrelstr (rng (f * d)) is strict full SubRelStr of BoolePoset X by Th1;
A28: rng ((g * f1) * (corestr c)) = the carrier of L by A21, FUNCT_2:def 3
.= dom (((inclusion c) * f) * d) by FUNCT_2:def 1 ;
p = (((((inclusion c) * f) * d) * g) * f1) * (corestr c) by RELAT_1:55
.= ((((inclusion c) * f) * d) * g) * (f1 * (corestr c)) by RELAT_1:55
.= (((inclusion c) * f) * d) * (g * (f1 * (corestr c))) by RELAT_1:55
.= (((inclusion c) * f) * d) * ((g * f1) * (corestr c)) by RELAT_1:55 ;
then rng (((inclusion c) * f) * d) = rng p by A28, RELAT_1:47;
hence L, Image p are_isomorphic by A22, A26, A27, YELLOW_0:def 15; :: thesis: verum