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;
assume A1: not L1 is finite ; :: thesis: CLweight L1 = CLweight (InclPoset (sigma L1))
A2: ( CLweight L1 = weight S & InclPoset the topology of S = InclPoset (sigma L1) ) by Th29, YELLOW_9:51;
RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of L1,the InternalRel of L1 #) by YELLOW_9:def 4;
then not S is finite by A1;
hence CLweight L1 = CLweight (InclPoset (sigma L1)) by A2, Th8; :: thesis: verum