theorem Th15: :: STACKS_1:15
for X being StackAlgebra
for s1, s2 being stack of X st emp s1 & emp s2 holds
s1 == s2