theorem Th19: :: STACKS_1:19

for X being StackAlgebra
for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X