let S be stack of (X /==); STACKS_1:def 11 for e being Element of (X /==) holds S = pop (push (e,S))
let E be Element of (X /==); S = pop (push (E,S))
consider s being stack of X such that
A20:
S = Class ((==_ X),s)
by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class ((==_ X),(push (e,s))) as stack of (X /==) by Th35;
A21:
not emp push (e,s)
by Def12;
thus S =
Class ((==_ X),(pop (push (e,s))))
by A20, Def11
.=
pop P
by A21, Th39
.=
pop (push (E,S))
by A20, Th38
; verum