set S = { (a * v) where v is Element of V : verum } ;

A1: now :: thesis: for x being object st x in { (a * v) where v is Element of V : verum } holds
x in the carrier of V

let x be object ; :: thesis: ( x in { (a * v) where v is Element of V : verum } implies x in the carrier of V )
assume x in { (a * v) where v is Element of V : verum } ; :: thesis: x in the carrier of V
then ex v being Element of V st x = a * v ;
hence x in the carrier of V ; :: thesis: verum

end;

a * (0. V) in { (a * v) where v is Element of V : verum } ;
hence { (a * v) where v is Element of V : verum } is non empty Subset of V by A1, TARSKI:def 3; :: thesis: verum