let X be StackAlgebra; for s being stack of X
for e being Element of X holds
( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
let s be stack of X; for e being Element of X holds
( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
let e be Element of X; ( s in coset (push (e,s)) & ( not emp s implies s in coset (pop s) ) )
( pop (push (e,s)) = s & not emp push (e,s) & push (e,s) in coset (push (e,s)) )
by Def11, Def12, Def17;
hence
s in coset (push (e,s))
by Def17; ( not emp s implies s in coset (pop s) )
assume
not emp s
; s in coset (pop s)
then
( push ((top s),(pop s)) = s & pop s in coset (pop s) )
by Def9, Def17;
hence
s in coset (pop s)
by Def17; verum