for X being non empty non void StackSystem st X is pop-finite holds
ex s being stack of X st emp s