let L1 be lower-bounded continuous sup-Semilattice; :: thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))
set S = the Scott TopAugmentation of L1;
A1: 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;
A2: InclPoset the topology of the Scott TopAugmentation of L1 = InclPoset (sigma L1) by YELLOW_9:51;
A3: CLweight L1 = weight the Scott TopAugmentation of L1 by Th24;

now :: thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))

per cases ( L1 is infinite or L1 is finite ) ;

suppose L1 is infinite ; :: thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))

then the Scott TopAugmentation of L1 is infinite by A1;
hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, Th6; :: thesis: verum

end;

suppose A4: L1 is finite ; :: thesis: CLweight L1 c= CLweight (InclPoset (sigma L1))

A5: card the carrier of the Scott TopAugmentation of L1 c= card the carrier of (InclPoset (sigma L1)) by A2, Th7;
A6: the Scott TopAugmentation of L1 is finite by A1, A4;
then weight the Scott TopAugmentation of L1 = card the carrier of the Scott TopAugmentation of L1 by Th8;
hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, A6, A5, Th9; :: thesis: verum

end;

end;

end;

hence CLweight L1 c= CLweight (InclPoset (sigma L1)) ; :: thesis: verum