defpred S₁[ object ] means ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & $1 in rng f );
thus for X1, X2 being set st ( for x being object holds
( x in X1 iff S₁[x] ) ) & ( for x being object holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from XBOOLE_0:sch 3(); :: thesis: verum