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