let S be stack of (X /==); :: according to STACKS_1:def 10 :: thesis: for e being Element of (X /==) holds e = top (push (e,S))
let E be Element of (X /==); :: thesis: E = top (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 E = top (push (e,s)) by TOPPUSH
.= top P by A2, Th74
.= top (push (E,S)) by A1, Th72 ; :: thesis: verum