defpred S₁[ stack of X, stack of X] means ( ( not emp $1 & $2 = pop $1 ) or ex e being Element of X st $2 = push (e,$1) );
let R1, R2 be Relation of the carrier' of X; :: thesis: ( ( for s1, s2 being stack of X holds
( [s1,s2] in R1 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) & ( for s1, s2 being stack of X holds
( [s1,s2] in R2 iff ( ( not emp s1 & s2 = pop s1 ) or ex e being Element of X st s2 = push (e,s1) ) ) ) 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