let X be non empty non void StackSystem ; :: thesis: ( X is pop-finite implies ex s being stack of X st emp s )
assume A0: X is pop-finite ; :: thesis: ex s being stack of X st emp s
set s1 = the stack of X;
defpred S₁[ set , stack of X, stack of X] means $3 = pop $2;
A1: for n being Element of NAT
for x being stack of X ex y being stack of X st S₁[n,x,y] ;
consider f being Function of NAT, the carrier' of X such that
A2: ( f . 0 = the stack of X & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
consider i being Nat, s being stack of X such that
A3: ( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) by A0, POPFIN;
take s ; :: thesis: emp s
i is Element of NAT by ORDINAL1:def 12;
hence emp s by A2, A3; :: thesis: verum