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
A1: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of L1,the InternalRel of L1 #) by YELLOW_9:def 4;
consider B1 being with_bottom CLbasis of L1 such that
A2: card B1 = CLweight L1 by Th4;

now

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

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

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

end;

suppose A5: not L1 is finite ; :: 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 ) } ;
A6: 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 A2, A5, Th24;
{ (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 Th26;
then 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:74;
hence weight T c= CLweight L1 by A6, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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