let L1 be finite LATTICE; :: thesis: for B1 being with_bottom CLbasis of L1 holds
( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )
let B1 be with_bottom CLbasis of L1; :: thesis: ( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )
thus ( card B1 = CLweight L1 implies B1 = the carrier of (CompactSublatt L1) ) :: thesis: ( B1 = the carrier of (CompactSublatt L1) implies card B1 = CLweight L1 )

proof

assume card B1 = CLweight L1 ; :: thesis: B1 = the carrier of (CompactSublatt L1)
then A1: card the carrier of (CompactSublatt L1) = card B1 by Th3;
the carrier of (CompactSublatt L1) c= B1 by WAYBEL23:71;
hence B1 = the carrier of (CompactSublatt L1) by A1, CARD_2:102; :: thesis: verum

end;

assume B1 = the carrier of (CompactSublatt L1) ; :: thesis: card B1 = CLweight L1
hence card B1 = CLweight L1 by Th3; :: thesis: verum