let X be non empty non void StackSystem ; :: thesis: ( X is pop-finite implies ex s being stack of X st emp s )
assume A1: 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;
A2: for n being Nat
for x being stack of X ex y being stack of X st S₁[n,x,y] ;
consider f being sequence of the carrier' of X such that
A3: ( f . 0 = the stack of X & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
consider i being Nat, s being stack of X such that
A4: ( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) by A1;
take s ; :: thesis: emp s
thus emp s by A3, A4; :: thesis: verum