let L1 be lower-bounded continuous sup-Semilattice; :: thesis: ( L1 is infinite implies CLweight L1 = CLweight (InclPoset (sigma L1)) )
set S = the Scott TopAugmentation of L1;
assume A1: L1 is infinite ; :: 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 Th24, 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 the Scott TopAugmentation of L1 is infinite by A1;
hence CLweight L1 = CLweight (InclPoset (sigma L1)) by A2, Th6; :: thesis: verum