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