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