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 & T, Image p are_isomorphic ) by WAYBEL13:35;
( p * p = p & (id S) * (id S) = id S ) by QUANTAL1:def 9;
then (UPS (id S),p) * (UPS (id S),p) = UPS (id S),p by A1, Th28;
then A2: 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;
UPS (id S),p is closure

proof

thus UPS (id S),p is projection by A2, WAYBEL_1:def 13; :: according to WAYBEL_1:def 14 :: thesis: id (UPS S,(BoolePoset X)) <= UPS (id S),p

now

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

now

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

end;

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

end;

hence id (UPS S,(BoolePoset X)) <= UPS (id S),p by YELLOW_2:10; :: thesis: verum

end;

then reconsider Sp = UPS (id S),p as directed-sups-preserving closure Function of (UPS S,(BoolePoset X)),(UPS S,(BoolePoset X)) by A1, Th30;
A5: Image Sp is complete LATTICE by YELLOW_2:32;
BoolePoset X,(BoolePoset 1) |^ X are_isomorphic by Th18;
then ( UPS S,(BoolePoset X), UPS S,((BoolePoset 1) |^ X) are_isomorphic & UPS S,((BoolePoset 1) |^ X),(UPS S,(BoolePoset 1)) |^ X are_isomorphic ) by Th36, Th42;
then A6: UPS S,(BoolePoset X),(UPS S,(BoolePoset 1)) |^ X are_isomorphic by WAYBEL_1:8;
consider L being Scott TopAugmentation of S;
A7: 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 A8: ( InclPoset (sigma S) is algebraic & InclPoset (sigma S) = InclPoset the topology of L ) by A7, YELLOW_9:51, 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 A8, WAYBEL13:32, WAYBEL_1:7;
then for x being Element of X holds (X --> (UPS S,(BoolePoset 1))) . x is lower-bounded algebraic LATTICE by FUNCOP_1:13;
then ( X -POS_prod (X --> (UPS S,(BoolePoset 1))) is lower-bounded & X -POS_prod (X --> (UPS S,(BoolePoset 1))) is algebraic ) by WAYBEL13:25;
then ( (UPS S,(BoolePoset 1)) |^ X is algebraic & (UPS S,(BoolePoset 1)) |^ X is lower-bounded ) by YELLOW_1:def 5;
then UPS S,(BoolePoset X) is lower-bounded algebraic LATTICE by A6, WAYBEL13:32, WAYBEL_1:7;
then A9: Image Sp is algebraic by WAYBEL_8:26;
Image p is non empty complete Poset by A1, WAYBEL20:18;
then UPS S,T, UPS S,(Image p) are_isomorphic by A1, Th36;
then UPS S,T, Image Sp are_isomorphic by A1, Th37;
hence UPS S,T is algebraic by A5, A9, WAYBEL13:32, WAYBEL_1:7; :: thesis: verum