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