let L1 be lower-bounded algebraic LATTICE; :: thesis: CLweight L1 = card the carrier of (CompactSublatt L1)
set CB = { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
the carrier of (CompactSublatt L1) is with_bottom CLbasis of L1 by WAYBEL23:71;
then A1: card the carrier of (CompactSublatt L1) in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
then A2: meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } c= card the carrier of (CompactSublatt L1) by SETFAM_1:3;

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

let X be set ; :: thesis: ( X in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } implies card the carrier of (CompactSublatt L1) c= X )
assume X in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ; :: thesis: card the carrier of (CompactSublatt L1) c= X
then consider B1 being with_bottom CLbasis of L1 such that
A3: X = card B1 ;
the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:71;
hence card the carrier of (CompactSublatt L1) c= X by A3, CARD_1:11; :: thesis: verum

end;

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