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
A1:
S = Class ((==_ X),s)
by Th70;
reconsider e = E as Element of X by QUOT;
reconsider P = Class ((==_ X),(push (e,s))) as stack of (X /==) by Th70a;
A2:
not emp push (e,s)
by PUSHNE;
thus S =
Class ((==_ X),(pop (push (e,s))))
by A1, POPPUSH
.=
pop P
by A2, Th73
.=
pop (push (E,S))
by A1, Th72
; verum