let S, T be complete algebraic LATTICE; 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;
then A7:
id (UPS (S,(BoolePoset X))) <= UPS ((id S),p)
by YELLOW_2:9;
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
;
then reconsider Sp = UPS ((id S),p) as directed-sups-preserving closure Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by A7, A1, Th30, WAYBEL_1:def 14;
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 {0}) |^ X are_isomorphic
by Th18;
then A10:
UPS (S,(BoolePoset X)), UPS (S,((BoolePoset {0}) |^ X)) are_isomorphic
by Th36;
set L = the Scott TopAugmentation of S;
A11:
InclPoset (sigma S) = InclPoset the topology of the Scott TopAugmentation of S
by YELLOW_9:51;
A12:
RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
then
the Scott TopAugmentation of S is algebraic
by WAYBEL13:26, WAYBEL13:32;
then
ex B being Basis of the Scott TopAugmentation of S st B = { (uparrow x) where x is Element of the Scott TopAugmentation of S : x in the carrier of (CompactSublatt the Scott TopAugmentation of S) }
by WAYBEL14:42;
then
InclPoset (sigma the Scott TopAugmentation of S) is algebraic
by WAYBEL14:43;
then A13:
InclPoset (sigma S) is algebraic
by A12, YELLOW_9:52;
UPS (S,(BoolePoset {0})), InclPoset (sigma S) are_isomorphic
by Th34;
then
( UPS (S,(BoolePoset {0})) is algebraic & UPS (S,(BoolePoset {0})) is lower-bounded )
by A13, A11, WAYBEL13:32, WAYBEL_1:6;
then
( X -POS_prod (X --> (UPS (S,(BoolePoset {0})))) is lower-bounded & X -POS_prod (X --> (UPS (S,(BoolePoset {0})))) is algebraic )
;
then A14:
( (UPS (S,(BoolePoset {0}))) |^ X is algebraic & (UPS (S,(BoolePoset {0}))) |^ X is lower-bounded )
by YELLOW_1:def 5;
UPS (S,((BoolePoset {0}) |^ X)),(UPS (S,(BoolePoset {0}))) |^ X are_isomorphic
by Th42;
then
UPS (S,(BoolePoset X)),(UPS (S,(BoolePoset {0}))) |^ X are_isomorphic
by A10, WAYBEL_1:7;
then
UPS (S,(BoolePoset X)) is lower-bounded algebraic LATTICE
by A14, WAYBEL13:32, WAYBEL_1:6;
then A15:
Image Sp is algebraic
by WAYBEL_8:24;
Image Sp is complete LATTICE
by YELLOW_2:30;
hence
UPS (S,T) is algebraic
by A9, A15, WAYBEL13:32, WAYBEL_1:6; verum