take { (a + W) where a is Vector of : verum } ; :: thesis: for x being set holds
( x in { (a + W) where a is Vector of : verum } iff ex a being Vector of st x = a + W )
thus for x being set holds
( x in { (a + W) where a is Vector of : verum } iff ex a being Vector of st x = a + W ) ; :: thesis: verum