let S be stack of (X /==); :: according to STACKS_1:def 12 :: thesis: for e being Element of (X /==) holds not emp push (e,S)
let E be Element of (X /==); :: thesis: not emp push (E,S)
consider s being stack of X such that
A22: 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;
not emp push (e,s) by Def12;
then not emp P by Th36;
hence not emp push (E,S) by A22, Th38; :: thesis: verum