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
now 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
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 #) &
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
(
TopStruct(# the
carrier of
(Sigma S),the
topology of
(Sigma S) #)
= TopStruct(# the
carrier of
SS,the
topology of
SS #) &
TopStruct(# the
carrier of
(Sigma L),the
topology of
(Sigma L) #)
= TopStruct(# the
carrier of
SL,the
topology of
SL #) )
by Th17;
then
[:SS,SL:] = [:(Sigma S),(Sigma L):]
by Th10;
hence
sigma [:S,L:] = the
topology of
[:SS,SL:]
by A1;
:: thesis: verum end;
hence
InclPoset (sigma L) is continuous
by Lm11; :: thesis: verum