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;

.= (((((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

( 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

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
(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;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

.= (((((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