let X be StackAlgebra; :: thesis: for s1, s2 being stack of X st emp s1 & emp s2 holds
s1 == s2
let s1, s2 be stack of X; :: thesis: ( emp s1 & emp s2 implies s1 == s2 )
assume ( emp s1 & emp s2 ) ; :: thesis: s1 == s2
then ( |.s1.| = {} & |.s2.| = {} ) by Th5;
hence |.s1.| = |.s2.| ; :: according to STACKS_1:def 14 :: thesis: verum