set A = Carrier L;
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds
L . v = 0 by Def3;
Carrier L c= T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in T )
assume x in Carrier L ; :: thesis: x in T
then ex v being Element of V st
( x = v & L . v <> 0 ) ;
hence x in T by A1; :: thesis: verum

end;

hence Carrier L is finite ; :: thesis: verum