let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T
let T be correct Lawson TopAugmentation of L1; :: thesis: CLweight L1 = weight T
set T1 = the Scott TopAugmentation of L1;
( CLweight L1 c= weight the Scott TopAugmentation of L1 & weight the Scott TopAugmentation of L1 c= weight T ) by Lm1, Lm3;
then A1: CLweight L1 c= weight T ;
weight T c= CLweight L1 by Lm2;
hence CLweight L1 = weight T by A1, XBOOLE_0:def 10; :: thesis: verum