let R be complete LATTICE; :: thesis: lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R)))
consider S being correct Lawson TopAugmentation of R;
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
then A2: sigma R = sigma S by YELLOW_9:52;
(omega S) \/ (sigma S) is prebasis of S by Def3;
then FinMeetCl ((omega S) \/ (sigma S)) is Basis of S by YELLOW_9:23;
then A3: the topology of S = UniCl (FinMeetCl ((omega S) \/ (sigma S))) by YELLOW_9:22;
omega R = omega S by A1, Th3;
hence lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) by A3, A1, A2, Def4; :: thesis: verum