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