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