defpred S₁[ set ] means ex a being Vector of V st $1 = a + W;
thus for S1, S2 being set st ( for x being set holds
( x in S1 iff S₁[x] ) ) & ( for x being set holds
( x in S2 iff S₁[x] ) ) holds
S1 = S2 from XFAMILY:sch 3(); :: thesis: verum