let L be complete LATTICE; :: thesis: ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )

thus ( InclPoset (sigma L) is continuous implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) by Lm10; :: thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) implies InclPoset (sigma L) is continuous )

assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; :: thesis: InclPoset (sigma L) is continuous

thus ( InclPoset (sigma L) is continuous implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) by Lm10; :: thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) implies InclPoset (sigma L) is continuous )

assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; :: thesis: InclPoset (sigma L) is continuous

now :: thesis: for SL being Scott TopAugmentation of L

for S being complete LATTICE

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

hence
InclPoset (sigma L) is continuous
by Lm11; :: thesis: verumfor S being complete LATTICE

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

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:]

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

then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13;

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

then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13;

then [:SS,SL:] = [:(Sigma S),(Sigma L):] by A2, Th7;

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

end;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:]

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

then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13;

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

then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology of SS #) by Th13;

then [:SS,SL:] = [:(Sigma S),(Sigma L):] by A2, Th7;

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