let X be StackAlgebra; :: thesis: for s being stack of X st |.s.| = {} holds
emp s
let s be stack of X; :: thesis: ( |.s.| = {} implies emp s )
assume ( |.s.| = {} & not emp s ) ; :: thesis: contradiction
then {} = <*(top s)*> ^ |.(pop s).| by Th6;
hence contradiction ; :: thesis: verum