let X be StackAlgebra; :: thesis: for s1, s2 being stack of X st s1 == s2 & emp s1 holds
emp s2
let s1, s2 be stack of X; :: thesis: ( s1 == s2 & emp s1 implies emp s2 )
assume A1: ( |.s1.| = |.s2.| & emp s1 ) ; :: according to STACKS_1:def 14 :: thesis: emp s2
assume not emp s2 ; :: thesis: contradiction
then |.s2.| = <*(top s2)*> ^ |.(pop s2).| by Th6;
hence contradiction by A1, Th5; :: thesis: verum