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 & T, Image p are_isomorphic ) by WAYBEL15:20;
( 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 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 A2: 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 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 A3: UPS S,(BoolePoset X),(UPS S,(BoolePoset 1)) |^ X are_isomorphic by WAYBEL_1:8;
consider L being Scott TopAugmentation of S;
( RelStr(# the carrier of L,the InternalRel of L #) = RelStr(# the carrier of S,the InternalRel of S #) & InclPoset (sigma L) is continuous ) by WAYBEL14:36, YELLOW_9:def 4;
then A4: InclPoset (sigma S) is continuous by YELLOW_9:52;
UPS S,(BoolePoset 1), InclPoset (sigma S) are_isomorphic by Th34;
then ( UPS S,(BoolePoset 1) is continuous & UPS S,(BoolePoset 1) is complete ) by A4, WAYBEL15:11, WAYBEL_1:7;
then for x being Element of X holds (X --> (UPS S,(BoolePoset 1))) . x is complete continuous LATTICE by FUNCOP_1:13;
then X -POS_prod (X --> (UPS S,(BoolePoset 1))) is continuous by WAYBEL20:34;
then (UPS S,(BoolePoset 1)) |^ X is continuous by YELLOW_1:def 5;
then UPS S,(BoolePoset X) is continuous LATTICE by A3, WAYBEL15:11, WAYBEL_1:7;
then A5: Image (UPS (id S),p) is continuous by A2, WAYBEL15:17;
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 (UPS (id S),p) are_isomorphic by A1, Th37;
hence UPS S,T is continuous by A5, WAYBEL15:11, WAYBEL_1:7; :: thesis: verum