set S = { (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

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

a * (0. V) in { (a * v) where v is Element of V : verum }
;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;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

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