let S be stack of (X /==); :: according to STACKS_1:def 9 :: thesis: ( not emp S implies S = push ((top S),(pop S)) )
consider s being stack of X such that
A16: S = Class ((==_ X),s) by Th34;
assume not emp S ; :: thesis: S = push ((top S),(pop S))
then A17: not emp s by A16, Th36;
reconsider P = Class ((==_ X),(pop s)) as stack of (X /==) by Th35;
reconsider E = top s as Element of (X /==) by Def20;
thus S = Class ((==_ X),(push ((top s),(pop s)))) by A16, A17, Def9
.= push (E,P) by Th38
.= push ((top S),P) by A16, A17, Th40
.= push ((top S),(pop S)) by A16, A17, Th39 ; :: thesis: verum