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 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 ; :: thesis: verum