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