let L1 be lower-bounded continuous sup-Semilattice; :: thesis: ( not L1 is finite implies CLweight L1 = CLweight (InclPoset (sigma L1)) )
consider S being Scott TopAugmentation of L1;
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of L1,the InternalRel of L1 #) by YELLOW_9:def 4;
assume A2: not L1 is finite ; :: thesis: CLweight L1 = CLweight (InclPoset (sigma L1))
A3: CLweight L1 = weight S by Th29;
A4: InclPoset the topology of S = InclPoset (sigma L1) by YELLOW_9:51;
not the carrier of S is finite by A1, A2;
then not S is finite ;
hence CLweight L1 = CLweight (InclPoset (sigma L1)) by A3, A4, Th8; :: thesis: verum