defpred S1[ object ] means ex B being Element of FX st
( B in FX & $1 = B \ (PartUnion (B,R)) );
thus
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 XFAMILY:sch 3(); verum