set X = StandardStackSystem A;
let s1, s2 be stack of (StandardStackSystem A); :: according to STACKS_1:def 15 :: thesis: ( s1 == s2 implies s1 = s2 )
assume |.s1.| = |.s2.| ; :: according to STACKS_1:def 14 :: thesis: s1 = s2
hence s1 = |.s2.| by Th11
.= s2 by Th11 ;
:: thesis: verum