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:20;
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;
consider L being Scott TopAugmentation of S;
A5: InclPoset (sigma L) is continuous by WAYBEL14:36;
A6: UPS S,(BoolePoset 1), 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 1) |^ X are_isomorphic by Th18;
then A8: UPS S,(BoolePoset X), UPS S,((BoolePoset 1) |^ X) are_isomorphic by Th36;
RelStr(# the carrier of L,the InternalRel of L #) = 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 1) is continuous & UPS S,(BoolePoset 1) is complete ) by A6, 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 A9: (UPS S,(BoolePoset 1)) |^ X is continuous 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 A8, WAYBEL_1:8;
then UPS S,(BoolePoset X) is continuous LATTICE by A9, WAYBEL15:11, WAYBEL_1:7;
then Image (UPS (id S),p) is continuous by A7, WAYBEL15:17;
hence UPS S,T is continuous by A4, WAYBEL15:11, WAYBEL_1:7; :: thesis: verum