let X be StackAlgebra; for s1, s2, s3 being stack of X st s1 == s2 & s2 == s3 holds
s1 == s3
let s1, s2, s3 be stack of X; ( s1 == s2 & s2 == s3 implies s1 == s3 )
assume
( |.s1.| = |.s2.| & |.s2.| = |.s3.| )
; STACKS_1:def 14 s1 == s3
hence
|.s1.| = |.s3.|
; STACKS_1:def 14 verum