let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
let T be correct Lawson TopAugmentation of L1; :: thesis: weight T c= CLweight L1
consider B1 being with_bottom CLbasis of L1 such that
A1: card B1 = CLweight L1 by Th2;
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def 4;

now :: thesis: weight T c= CLweight L1

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

suppose A3: L1 is finite ; :: thesis: weight T c= CLweight L1

then A4: T is finite by A2;
B1 = the carrier of (CompactSublatt L1) by A1, A3, Th13
.= the carrier of L1 by A3, YELLOW15:26 ;
hence weight T c= CLweight L1 by A2, A1, A4, Th8; :: thesis: verum

end;

suppose A5: L1 is infinite ; :: thesis: weight T c= CLweight L1

set WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } ;
{ (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T by Th21;
then A6: weight T c= card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } by WAYBEL23:73;
card { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= CLweight L1 by A1, A5, Th19;
hence weight T c= CLweight L1 by A6; :: thesis: verum

end;

end;

end;

hence weight T c= CLweight L1 ; :: thesis: verum