let S, T be complete continuous LATTICE; :: thesis: UPS (S,T) is continuous
consider X being non empty set , p being projection Function of (BoolePoset X),(BoolePoset X) such that
A1: p is directed-sups-preserving and
A2: T, Image p are_isomorphic by WAYBEL15:18;
A3: (id S) * (id S) = id S by QUANTAL1:def 9;
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 A4: UPS (S,T), Image (UPS ((id S),p)) are_isomorphic by A1, Th37;
set L = the Scott TopAugmentation of S;
A5: InclPoset (sigma the Scott TopAugmentation of S) is continuous by WAYBEL14:36;
A6: UPS (S,(BoolePoset {0})), InclPoset (sigma S) are_isomorphic by Th34;
p * p = p by QUANTAL1:def 9;
then (UPS ((id S),p)) * (UPS ((id S),p)) = UPS ((id S),p) by A3, 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 A7: UPS ((id S),p) is directed-sups-preserving projection Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by WAYBEL_1:def 13;
BoolePoset X,(BoolePoset {0}) |^ X are_isomorphic by Th18;
then A8: UPS (S,(BoolePoset X)), UPS (S,((BoolePoset {0}) |^ X)) are_isomorphic by Th36;
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 InclPoset (sigma S) is continuous by A5, YELLOW_9:52;
then ( UPS (S,(BoolePoset {0})) is continuous & UPS (S,(BoolePoset {0})) is complete ) by A6, WAYBEL15:9, WAYBEL_1:6;
then for x being Element of X holds (X --> (UPS (S,(BoolePoset {0})))) . x is complete continuous LATTICE ;
then X -POS_prod (X --> (UPS (S,(BoolePoset {0})))) is continuous by WAYBEL20:33;
then A9: (UPS (S,(BoolePoset {0}))) |^ X is continuous 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 A8, WAYBEL_1:7;
then UPS (S,(BoolePoset X)) is continuous LATTICE by A9, WAYBEL15:9, WAYBEL_1:6;
then Image (UPS ((id S),p)) is continuous by A7, WAYBEL15:15;
hence UPS (S,T) is continuous by A4, WAYBEL15:9, WAYBEL_1:6; :: thesis: verum