let L be complete LATTICE; ( 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; ( ( 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):]
; InclPoset (sigma L) is continuous
now 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:]let SL be
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:]let S be
complete LATTICE;
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]let SS be
Scott TopAugmentation of
S;
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;
verum end;
hence
InclPoset (sigma L) is continuous
by Lm11; verum