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

now

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

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

then not S is finite by A1;
hence CLweight L1 c= CLweight (InclPoset (sigma L1)) by A3, A2, Th8; :: thesis: verum

end;

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

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

end;

end;

end;

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