defpred S₁[ object ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 or $1 = x6 or $1 = x7 or $1 = x8 or $1 = x9 or $1 = x10 );
thus for X, Y being set st ( for x being object holds
( x in X iff S₁[x] ) ) & ( for x being object holds
( x in Y iff S₁[x] ) ) holds
X = Y from XBOOLE_0:sch 3(); :: thesis: verum