let R be complete LATTICE; for T being correct lower TopAugmentation of R
for S being correct Scott TopAugmentation of R
for M being Refinement of S,T holds lambda R = the topology of M
let T be correct lower TopAugmentation of R; for S being correct Scott TopAugmentation of R
for M being Refinement of S,T holds lambda R = the topology of M
let S be correct Scott TopAugmentation of R; for M being Refinement of S,T holds lambda R = the topology of M
let M be Refinement of S,T; lambda R = the topology of M
A1:
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #)
by YELLOW_9:def 4;
A2:
the carrier of R \/ the carrier of R = the carrier of R
;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #)
by YELLOW_9:def 4;
then A3:
the carrier of M = the carrier of R
by A2, A1, YELLOW_9:def 6;
A4:
sigma R = the topology of S
by YELLOW_9:51;
omega R = the topology of T
by Def2;
then
(sigma R) \/ (omega R) is prebasis of M
by A4, YELLOW_9:def 6;
then A5:
FinMeetCl ((sigma R) \/ (omega R)) is Basis of M
by A3, YELLOW_9:23;
thus lambda R =
UniCl (FinMeetCl ((sigma R) \/ (omega R)))
by Th33
.=
the topology of M
by A3, A5, YELLOW_9:22
; verum