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
A18: 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;
A19: not emp push (e,s) by Def12;
thus E = top (push (e,s)) by Def10
.= top P by A19, Th40
.= top (push (E,S)) by A18, Th38 ; :: thesis: verum