defpred S1[ set ] means ex W being strict Submodule of V st W = $1;
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2
from XBOOLE_0:sch 3();
hence
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Submodule of V st W = x ) ) & ( for x being set holds
( x in b2 iff ex W being strict Submodule of V st W = x ) ) holds
b1 = b2
; verum