let S be stack of (X /==); STACKS_1:def 9 ( 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
; 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
; verum