defpred S₁[ stack of X, stack of X] means $1 == $2;
thus ex R being Relation of the carrier' of X st
for s1, s2 being stack of X holds
( [s1,s2] in R iff S₁[s1,s2] ) from RELSET_1:sch 2(); :: thesis: verum