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 = 0c by Def1;

now

let x be set ; :: thesis: ( x in Carrier L implies x in T )
assume x in Carrier L ; :: thesis: x in T
then ex v being Element of V st
( x = v & L . v <> 0c ) ;
hence x in T by A1; :: thesis: verum

end;

then Carrier L c= T by TARSKI:def 3;
hence Carrier L is finite ; :: thesis: verum