let L be complete LATTICE; :: thesis: ( S_{8}[L] iff S_{9}[L] )

thus ( S_{8}[L] implies S_{9}[L] )
:: thesis: ( S_{9}[L] implies S_{8}[L] )_{9}[L]
; :: thesis: S_{8}[L]

let SL be Scott TopAugmentation of L; :: thesis: for S being complete LATTICE

for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]

let S be complete LATTICE; :: thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]

let SS be Scott TopAugmentation of S; :: thesis: sigma [:S,L:] = the topology of [:SS,SL:]

thus ( S

proof

assume A4:
S
assume A1:
S_{8}[L]
; :: thesis: S_{9}[L]

let SL be Scott TopAugmentation of L; :: thesis: for S being complete LATTICE

for SS being Scott TopAugmentation of S

for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

let S be complete LATTICE; :: thesis: for SS being Scott TopAugmentation of S

for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

let SS be Scott TopAugmentation of S; :: thesis: for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

let SSL be Scott TopAugmentation of [:S,L:]; :: thesis: TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

A2: the topology of [:SS,SL:] = sigma [:S,L:] by A1

.= the topology of SSL by YELLOW_9:51 ;

A3: RelStr(# the carrier of SSL, the InternalRel of SSL #) = RelStr(# the carrier of [:S,L:], the InternalRel of [:S,L:] #) by YELLOW_9:def 4;

( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def 4;

then the carrier of SSL = [: the carrier of SS, the carrier of SL:] by A3, YELLOW_3:def 2

.= the carrier of [:SS,SL:] by BORSUK_1:def 2 ;

hence TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] by A2; :: thesis: verum

end;let SL be Scott TopAugmentation of L; :: thesis: for S being complete LATTICE

for SS being Scott TopAugmentation of S

for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

let S be complete LATTICE; :: thesis: for SS being Scott TopAugmentation of S

for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

let SS be Scott TopAugmentation of S; :: thesis: for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

let SSL be Scott TopAugmentation of [:S,L:]; :: thesis: TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]

A2: the topology of [:SS,SL:] = sigma [:S,L:] by A1

.= the topology of SSL by YELLOW_9:51 ;

A3: RelStr(# the carrier of SSL, the InternalRel of SSL #) = RelStr(# the carrier of [:S,L:], the InternalRel of [:S,L:] #) by YELLOW_9:def 4;

( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def 4;

then the carrier of SSL = [: the carrier of SS, the carrier of SL:] by A3, YELLOW_3:def 2

.= the carrier of [:SS,SL:] by BORSUK_1:def 2 ;

hence TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] by A2; :: thesis: verum

let SL be Scott TopAugmentation of L; :: thesis: for S being complete LATTICE

for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]

let S be complete LATTICE; :: thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]

let SS be Scott TopAugmentation of S; :: thesis: sigma [:S,L:] = the topology of [:SS,SL:]

now :: thesis: for SSL being Scott TopAugmentation of [:S,L:] holds sigma [:S,L:] = the topology of [:SS,SL:]

hence
sigma [:S,L:] = the topology of [:SS,SL:]
; :: thesis: verumlet SSL be Scott TopAugmentation of [:S,L:]; :: thesis: sigma [:S,L:] = the topology of [:SS,SL:]

TopStruct(# the carrier of SSL, the topology of SSL #) = TopStruct(# the carrier of [:SS,SL:], the topology of [:SS,SL:] #) by A4;

hence sigma [:S,L:] = the topology of [:SS,SL:] by YELLOW_9:51; :: thesis: verum

end;TopStruct(# the carrier of SSL, the topology of SSL #) = TopStruct(# the carrier of [:SS,SL:], the topology of [:SS,SL:] #) by A4;

hence sigma [:S,L:] = the topology of [:SS,SL:] by YELLOW_9:51; :: thesis: verum