let X be StackAlgebra; for s being stack of X st emp s holds
Class ((==_ X),s) = the s_empty of X
let s be stack of X; ( emp s implies Class ((==_ X),s) = the s_empty of X )
assume A1:
emp s
; Class ((==_ X),s) = the s_empty of X
thus
Class ((==_ X),s) c= the s_empty of X
XBOOLE_0:def 10 the s_empty of X c= Class ((==_ X),s)
let x be object ; TARSKI:def 3 ( not x in the s_empty of X or x in Class ((==_ X),s) )
assume A3:
x in the s_empty of X
; x in Class ((==_ X),s)
then reconsider s1 = x as stack of X ;
emp s1
by A3;
then
s == s1
by A1, Th15;
then
[s,s1] in ==_ X
by Def16;
hence
x in Class ((==_ X),s)
by EQREL_1:18; verum