defpred S₁[ stack of X, stack of X] means $1 == $2;
let R1, R2 be Relation of the carrier' of X; :: thesis: ( ( for s1, s2 being stack of X holds
( [s1,s2] in R1 iff s1 == s2 ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in R2 iff s1 == s2 ) ) implies R1 = R2 )
assume that
A1: for s1, s2 being stack of X holds
( [s1,s2] in R1 iff S₁[s1,s2] ) and
A2: for s1, s2 being stack of X holds
( [s1,s2] in R2 iff S₁[s1,s2] ) ; :: thesis: R1 = R2
thus R1 = R2 from RELSET_1:sch 4(A1, A2); :: thesis: verum