defpred S1[ stack of X, stack of X] means $1 == $2;
let R1, R2 be Relation of the carrier' of X; ( ( 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 S1[s1,s2] )
and
A2:
for s1, s2 being stack of X holds
( [s1,s2] in R2 iff S1[s1,s2] )
; R1 = R2
thus
R1 = R2
from RELSET_1:sch 4(A1, A2); verum