set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def 12 :: thesis: for e being Element of (StandardStackSystem A) holds not emp push (e,s)
let e be Element of (StandardStackSystem A); :: thesis: not emp push (e,s)
reconsider g = s as Element of A * by Def7;
push (e,s) = <*e*> ^ g by Def7;
hence not emp push (e,s) by Def7; :: thesis: verum