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