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