let X be StackAlgebra; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: ( not emp s implies s in coset (pop s) )
assume not emp s ; :: thesis: 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; :: thesis: verum