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
consider T1 being correct Lawson TopAugmentation of L1;
A1: CLweight L1 c= weight T by Lm3;
A2: weight T c= weight T1 by Lm1;
weight T1 c= CLweight L1 by Lm2;
then weight T c= CLweight L1 by A2, XBOOLE_1:1;
hence CLweight L1 = weight T by A1, XBOOLE_0:def 10; :: thesis: verum