let L be complete LATTICE; :: thesis: ( S8[L] implies S7[L] )
set SL = the Scott TopAugmentation of L;
A1: RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4;
TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) = ConvergenceSpace () by WAYBEL11:32;
then A2: the topology of the Scott TopAugmentation of L = sigma the Scott TopAugmentation of L ;
then A3: InclPoset () = InclPoset the topology of the Scott TopAugmentation of L by ;
then reconsider S = InclPoset () as complete LATTICE ;
set SS = the Scott TopAugmentation of S;
assume S8[L] ; :: thesis: S7[L]
then A4: sigma [:S,L:] = the topology of [: the Scott TopAugmentation of S, the Scott TopAugmentation of L:] ;
A5: S5[ the Scott TopAugmentation of L]
proof
set Wy = { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } ;
let T be Scott TopAugmentation of InclPoset the topology of the Scott TopAugmentation of L; :: thesis: { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } is open Subset of [:T, the Scott TopAugmentation of L:]
{ [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } c= the carrier of [:T, the Scott TopAugmentation of L:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } or x in the carrier of [:T, the Scott TopAugmentation of L:] )
A6: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of the Scott TopAugmentation of L), the InternalRel of (InclPoset the topology of the Scott TopAugmentation of L) #) by YELLOW_9:def 4;
assume x in { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } ; :: thesis: x in the carrier of [:T, the Scott TopAugmentation of L:]
then consider W being open Subset of the Scott TopAugmentation of L, y being Element of the Scott TopAugmentation of L such that
A7: x = [W,y] and
y in W ;
W in the topology of the Scott TopAugmentation of L by PRE_TOPC:def 2;
then W in the carrier of (InclPoset the topology of the Scott TopAugmentation of L) by YELLOW_1:1;
then [W,y] in [: the carrier of T, the carrier of the Scott TopAugmentation of L:] by ;
hence x in the carrier of [:T, the Scott TopAugmentation of L:] by ; :: thesis: verum
end;
then reconsider WY = { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } as Subset of [:T, the Scott TopAugmentation of L:] ;
A8: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of (InclPoset the topology of the Scott TopAugmentation of L), the InternalRel of (InclPoset the topology of the Scott TopAugmentation of L) #) by
.= RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4 ;
reconsider T1 = T as Scott TopAugmentation of S by ;
A9: 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;
the carrier of [:T, the Scott TopAugmentation of L:] = [: the carrier of T, the carrier of the Scott TopAugmentation of L:] by BORSUK_1:def 2
.= the carrier of [:S,L:] by ;
then reconsider wy = WY as Subset of [:S,L:] ;
A10: wy is inaccessible
proof
let D be non empty directed Subset of [:S,L:]; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" (D,[:S,L:]) in wy or not D misses wy )
assume sup D in wy ; :: thesis: not D misses wy
then [(sup ()),(sup ())] in wy by YELLOW_3:46;
then consider sp1D being open Subset of the Scott TopAugmentation of L, sp2D being Element of the Scott TopAugmentation of L such that
A11: [(sup ()),(sup ())] = [sp1D,sp2D] and
A12: sp2D in sp1D ;
reconsider sp1D9 = sp1D as Subset of L by A1;
reconsider sp1D9 = sp1D9 as upper inaccessible Subset of L by ;
reconsider pD = proj1 D as Subset of (InclPoset the topology of the Scott TopAugmentation of L) by ;
reconsider proj2D = proj2 D as non empty directed Subset of L by ;
A13: sup () = union pD by ;
sup proj2D in sp1D9 by ;
then proj2 D meets sp1D by WAYBEL11:def 1;
then consider d being object such that
A14: d in proj2 D and
A15: d in sp1D by XBOOLE_0:3;
reconsider d = d as Element of L by A14;
d in sup () by ;
then consider V being set such that
A16: d in V and
A17: V in proj1 D by ;
consider Y being object such that
A18: [Y,d] in D by ;
reconsider V = V as Element of S by A17;
consider e being object such that
A19: [V,e] in D by ;
A20: Y in proj1 D by ;
A21: e in proj2 D by ;
reconsider Y = Y as Element of S by A20;
reconsider e = e as Element of L by A21;
consider DD being Element of [:S,L:] such that
A22: DD in D and
A23: [V,e] <= DD and
A24: [Y,d] <= DD by ;
D c= the carrier of [:S,L:] ;
then D c= [: the carrier of S, the carrier of L:] by YELLOW_3:def 2;
then consider DD1, DD2 being object such that
A25: DD = [DD1,DD2] by ;
A26: DD2 in proj2 D by ;
A27: DD1 in proj1 D by ;
reconsider DD2 = DD2 as Element of L by A26;
reconsider DD1 = DD1 as Element of S by A27;
[V,e] <= [DD1,DD2] by ;
then V <= DD1 by YELLOW_3:11;
then A28: V c= DD1 by YELLOW_1:3;
DD1 in the carrier of S ;
then DD1 in sigma L by YELLOW_1:1;
then DD1 in the topology of the Scott TopAugmentation of L by ;
then DD1 is open Subset of the Scott TopAugmentation of L by PRE_TOPC:def 2;
then A29: DD1 is upper Subset of L by ;
[Y,d] <= [DD1,DD2] by ;
then d <= DD2 by YELLOW_3:11;
then A30: DD2 in DD1 by ;
DD1 in the carrier of S ;
then DD1 in sigma L by YELLOW_1:1;
then DD1 in the topology of the Scott TopAugmentation of L by ;
then reconsider DD1 = DD1 as open Subset of the Scott TopAugmentation of L by PRE_TOPC:def 2;
reconsider DD2 = DD2 as Element of the Scott TopAugmentation of L by A1;
[DD1,DD2] in wy by A30;
hence not D misses wy by ; :: thesis: verum
end;
wy is upper
proof
let x, y be Element of [:S,L:]; :: according to WAYBEL_0:def 20 :: thesis: ( not x in wy or not x <= y or y in wy )
assume that
A31: x in wy and
A32: x <= y ; :: thesis: y in wy
consider x1 being open Subset of the Scott TopAugmentation of L, x2 being Element of the Scott TopAugmentation of L such that
A33: x = [x1,x2] and
A34: x2 in x1 by A31;
reconsider u2 = x2 as Element of L by A1;
x1 in the topology of the Scott TopAugmentation of L by PRE_TOPC:def 2;
then x1 in sigma L by ;
then reconsider u1 = x1 as Element of S by YELLOW_1:1;
the carrier of [:S,L:] = [: the carrier of S, the carrier of L:] by YELLOW_3:def 2;
then consider y1, y2 being object such that
A35: y1 in the carrier of S and
A36: y2 in the carrier of L and
A37: y = [y1,y2] by ZFMISC_1:def 2;
y1 in sigma L by ;
then y1 in the topology of the Scott TopAugmentation of L by ;
then reconsider y1 = y1 as open Subset of the Scott TopAugmentation of L by PRE_TOPC:def 2;
reconsider y2 = y2 as Element of the Scott TopAugmentation of L by ;
reconsider v2 = y2 as Element of L by A36;
y1 in the topology of the Scott TopAugmentation of L by PRE_TOPC:def 2;
then y1 in sigma L by ;
then reconsider v1 = y1 as Element of S by YELLOW_1:1;
A38: [u1,u2] <= [v1,v2] by ;
then u2 <= v2 by YELLOW_3:11;
then x2 <= y2 by ;
then A39: y2 in x1 by ;
u1 <= v1 by ;
then x1 c= y1 by YELLOW_1:3;
hence y in wy by ; :: thesis: verum
end;
then A40: wy in the topology of by ;
the topology of the Scott TopAugmentation of S = sigma S by YELLOW_9:51
.= the topology of T1 by YELLOW_9:51
.= the topology of T ;
then A41: TopStruct(# the carrier of the Scott TopAugmentation of S, the topology of the Scott TopAugmentation of S #) = TopStruct(# the carrier of T, the topology of T #) by A8;
TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) = TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) ;
then [: the Scott TopAugmentation of S, the Scott TopAugmentation of L:] = [:T, the Scott TopAugmentation of L:] by ;
hence { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } is open Subset of [:T, the Scott TopAugmentation of L:] by ; :: thesis: verum
end;
( S5[ the Scott TopAugmentation of L] implies InclPoset the topology of the Scott TopAugmentation of L is continuous )
proof end;
hence S7[L] by A1, A2, A5, YELLOW_9:52; :: thesis: verum