set A = { v where v is Element of V : L . v <> 0c } ;
for x being set st x in { v where v is Element of V : L . v <> 0c } holds
x in the carrier of V

proof

let x be set ; :: thesis: ( x in { v where v is Element of V : L . v <> 0c } implies x in the carrier of V )
assume x in { v where v is Element of V : L . v <> 0c } ; :: thesis: x in the carrier of V
then ex v being Element of V st
( x = v & L . v <> 0c ) ;
hence x in the carrier of V ; :: thesis: verum

end;

hence { v where v is Element of V : L . v <> 0c } is Subset of V by TARSKI:def 3; :: thesis: verum