let T be TopStruct ; :: thesis: for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds
CLweight L1 = card the carrier of L1
let L1 be lower-bounded continuous LATTICE; :: thesis: ( InclPoset the topology of T = L1 & T is finite implies CLweight L1 = card the carrier of L1 )
assume A1: InclPoset the topology of T = L1 ; :: thesis: ( not T is finite or CLweight L1 = card the carrier of L1 )
[#] L1 is with_bottom CLbasis of L1 by YELLOW15:25;
then A2: card the carrier of L1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
A3: CLweight L1 c= card the carrier of L1 by A2, SETFAM_1:def 1;
assume A4: T is finite ; :: thesis: CLweight L1 = card the carrier of L1

now :: thesis: for Z being set st Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } holds
card the carrier of L1 c= Z

let Z be set ; :: thesis: ( Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } implies card the carrier of L1 c= Z )
assume Z in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; :: thesis: card the carrier of L1 c= Z
then consider B1 being with_bottom CLbasis of L1 such that
A5: Z = card B1 ;
Bottom L1 in B1 by WAYBEL23:def 8;
then the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:48;
then A6: card the carrier of (CompactSublatt L1) c= card B1 by CARD_1:11;
L1 is finite by A1, A4, YELLOW_1:1;
hence card the carrier of L1 c= Z by A5, A6, YELLOW15:26; :: thesis: verum

end;

then card the carrier of L1 c= meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } by A2, SETFAM_1:5;
hence CLweight L1 = card the carrier of L1 by A3, XBOOLE_0:def 10; :: thesis: verum