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