let X be StackAlgebra; :: thesis: for S being stack of (X /==) holds
( emp S iff S = the s_empty of X )
let S be stack of (X /==); :: thesis: ( emp S iff S = the s_empty of X )
the carrier' of (X /==) = Class (==_ X) by Def20;
then S in Class (==_ X) ;
then consider x being object such that
A1: ( x in the carrier' of X & S = Class ((==_ X),x) ) by EQREL_1:def 3;
reconsider x = x as stack of X by A1;

hereby :: thesis: ( S = the s_empty of X implies emp S )

assume emp S ; :: thesis: S = the s_empty of X
then emp x by A1, Th36;
hence S = the s_empty of X by A1, Th19; :: thesis: verum

end;

assume S = the s_empty of X ; :: thesis: emp S
then x in the s_empty of X by A1, EQREL_1:20;
then emp x ;
hence emp S by A1, Th36; :: thesis: verum