let S, T be complete algebraic LATTICE; :: thesis: UPS S,T is algebraic
consider X being non empty set , p being closure Function of (BoolePoset X),(BoolePoset X) such that
A1: p is directed-sups-preserving and
A2: T, Image p are_isomorphic by WAYBEL13:35;

now

let i be Element of (UPS S,(BoolePoset X)); :: thesis: (id (UPS S,(BoolePoset X))) . i <= (UPS (id S),p) . i
reconsider f = i as directed-sups-preserving Function of S,(BoolePoset X) by Def4;
A3: (UPS (id S),p) . f = (p * f) * (id the carrier of S) by A1, Def5
.= p * f by FUNCT_2:23 ;

A4: now

let s be Element of S; :: thesis: i . s <= ((UPS (id S),p) . i) . s
A5: id (BoolePoset X) <= p by WAYBEL_1:def 14;
A6: (id (BoolePoset X)) . (i . s) = i . s by FUNCT_1:35;
(p * f) . s = p . (f . s) by FUNCT_2:21;
hence i . s <= ((UPS (id S),p) . i) . s by A5, A6, A3, YELLOW_2:10; :: thesis: verum

end;

(id (UPS S,(BoolePoset X))) . i = i by FUNCT_1:35;
hence (id (UPS S,(BoolePoset X))) . i <= (UPS (id S),p) . i by A4, Th23; :: thesis: verum

end;

then A7: id (UPS S,(BoolePoset X)) <= UPS (id S),p by YELLOW_2:10;
A8: (id S) * (id S) = id S by QUANTAL1:def 9;
p * p = p by QUANTAL1:def 9;
then (UPS (id S),p) * (UPS (id S),p) = UPS (id S),p by A8, A1, Th28;
then UPS (id S),p is idempotent directed-sups-preserving Function of (UPS S,(BoolePoset X)),(UPS S,(BoolePoset X)) by A1, Th30, QUANTAL1:def 9;
then UPS (id S),p is projection by WAYBEL_1:def 13;
then reconsider Sp = UPS (id S),p as directed-sups-preserving closure Function of (UPS S,(BoolePoset X)),(UPS S,(BoolePoset X)) by A7, WAYBEL_1:def 14, A1, Th30;
Image p is non empty complete Poset by A2, WAYBEL20:18;
then UPS S,T, UPS S,(Image p) are_isomorphic by A2, Th36;
then A9: UPS S,T, Image Sp are_isomorphic by A1, Th37;
BoolePoset X,(BoolePoset 1) |^ X are_isomorphic by Th18;
then A10: UPS S,(BoolePoset X), UPS S,((BoolePoset 1) |^ X) are_isomorphic by Th36;
consider L being Scott TopAugmentation of S;
A11: InclPoset (sigma S) = InclPoset the topology of L by YELLOW_9:51;
A12: RelStr(# the carrier of L,the InternalRel of L #) = RelStr(# the carrier of S,the InternalRel of S #) by YELLOW_9:def 4;
then L is algebraic by WAYBEL13:26, WAYBEL13:32;
then ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } by WAYBEL14:42;
then InclPoset (sigma L) is algebraic by WAYBEL14:43;
then A13: InclPoset (sigma S) is algebraic by A12, YELLOW_9:52;
UPS S,(BoolePoset 1), InclPoset (sigma S) are_isomorphic by Th34;
then ( UPS S,(BoolePoset 1) is algebraic & UPS S,(BoolePoset 1) is lower-bounded ) by A13, A11, WAYBEL13:32, WAYBEL_1:7;
then ( X -POS_prod (X --> (UPS S,(BoolePoset 1))) is lower-bounded & X -POS_prod (X --> (UPS S,(BoolePoset 1))) is algebraic ) ;
then A14: ( (UPS S,(BoolePoset 1)) |^ X is algebraic & (UPS S,(BoolePoset 1)) |^ X is lower-bounded ) by YELLOW_1:def 5;
UPS S,((BoolePoset 1) |^ X),(UPS S,(BoolePoset 1)) |^ X are_isomorphic by Th42;
then UPS S,(BoolePoset X),(UPS S,(BoolePoset 1)) |^ X are_isomorphic by A10, WAYBEL_1:8;
then UPS S,(BoolePoset X) is lower-bounded algebraic LATTICE by A14, WAYBEL13:32, WAYBEL_1:7;
then A15: Image Sp is algebraic by WAYBEL_8:26;
Image Sp is complete LATTICE by YELLOW_2:32;
hence UPS S,T is algebraic by A9, A15, WAYBEL13:32, WAYBEL_1:7; :: thesis: verum