defpred S1[ 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 );
for X1, X2 being set st ( for x being object holds
( x in X1 iff S1[x] ) ) & ( for x being object 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 object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being object holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) holds
b1 = b2
; verum