let S1, S2 be stack of (X /==); :: according to STACKS_1:def 15 :: thesis: ( S1 == S2 implies S1 = S2 )
consider s1 being stack of X such that
A1: S1 = Class ((==_ X),s1) by Th34;
consider s2 being stack of X such that
A2: S2 = Class ((==_ X),s2) by Th34;
assume |.S1.| = |.S2.| ; :: according to STACKS_1:def 14 :: thesis: S1 = S2
then |.s1.| = |.S2.| by A1, Th41
.= |.s2.| by A2, Th41 ;
then s1 == s2 ;
then [s1,s2] in ==_ X by Def16;
then s2 in S1 by A1, EQREL_1:18;
hence S1 = S2 by A1, A2, EQREL_1:23; :: thesis: verum