let R be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: for M being Refinement of S,T holds lambda R = the topology of M
let M be Refinement of S,T; :: thesis: lambda R = the topology of M
A1: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of R,the InternalRel of R #) & RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) ) by YELLOW_9:def 4;
( sigma R = the topology of S & omega R = the topology of T & the carrier of R \/ the carrier of R = the carrier of R ) by Def2, YELLOW_9:51;
then A2: ( (sigma R) \/ (omega R) is prebasis of M & the carrier of M = the carrier of R ) by A1, YELLOW_9:def 6;
then A3: FinMeetCl ((sigma R) \/ (omega R)) is Basis of M by YELLOW_9:23;
thus lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) by Th33
.= the topology of M by A2, A3, YELLOW_9:22 ; :: thesis: verum