let X be StackAlgebra; :: thesis: for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X
let s be stack of X; :: thesis: ( emp s implies Class ((==_ X),s) = the s_empty of X )
assume Z0: emp s ; :: thesis: Class ((==_ X),s) = the s_empty of X
thus Class ((==_ X),s) c= the s_empty of X :: according to XBOOLE_0:def 10 :: thesis: the s_empty of X c= Class ((==_ X),s)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Class ((==_ X),s) or x in the s_empty of X )
assume Z1: x in Class ((==_ X),s) ; :: thesis: x in the s_empty of X
then reconsider s1 = x as stack of X ;
[s,s1] in ==_ X by Z1, EQREL_1:18;
then s == s1 by REL;
then emp s1 by Z0, Th42;
hence x in the s_empty of X by EMP; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the s_empty of X or x in Class ((==_ X),s) )
assume Z2: x in the s_empty of X ; :: thesis: x in Class ((==_ X),s)
then reconsider s1 = x as stack of X ;
emp s1 by Z2, EMP;
then s == s1 by Z0, Th43;
then [s,s1] in ==_ X by REL;
hence x in Class ((==_ X),s) by EQREL_1:18; :: thesis: verum