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