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