let L be complete LATTICE; :: thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]),the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] )
hereby :: thesis: ( ( for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]),the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )
assume A1:
for
S being
complete LATTICE holds
sigma [:S,L:] = the
topology of
[:(Sigma S),(Sigma L):]
;
:: thesis: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]),the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]
S8[
L]
proof
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
for
S being
complete LATTICE holds
TopStruct(# the
carrier of
(Sigma [:S,L:]),the
topology of
(Sigma [:S,L:]) #)
= [:(Sigma S),(Sigma L):]
by Lm9;
:: thesis: verum
end;
assume A2:
for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]),the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]
; :: thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
let S be complete LATTICE; :: thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
TopStruct(# the carrier of (Sigma [:S,L:]),the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]
by A2;
hence
sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
by YELLOW_9:51; :: thesis: verum