ex s being stack of X st emp s by Th2;
hence not the s_empty of X is empty ; :: thesis: verum