take
{ (a + W) where a is Vector of V : verum }
; :: thesis: for x being set holds

( x in { (a + W) where a is Vector of V : verum } iff ex a being Vector of V st x = a + W )

thus for x being set holds

( x in { (a + W) where a is Vector of V : verum } iff ex a being Vector of V st x = a + W ) ; :: thesis: verum

( x in { (a + W) where a is Vector of V : verum } iff ex a being Vector of V st x = a + W )

thus for x being set holds

( x in { (a + W) where a is Vector of V : verum } iff ex a being Vector of V st x = a + W ) ; :: thesis: verum