defpred S₁[ set ] means $1 is_/\-irreducible_in X;
thus for X1, X2 being Subset of X st ( for y being set holds
( y in X1 iff S₁[y] ) ) & ( for y being set holds
( y in X2 iff S₁[y] ) ) holds
X1 = X2 from ARMSTRNG:sch 1(); :: thesis: verum