let X be StackAlgebra; for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) holds
( emp s iff emp S )
let s be stack of X; for S being stack of (X /==) st S = Class ((==_ X),s) holds
( emp s iff emp S )
let S be stack of (X /==); ( S = Class ((==_ X),s) implies ( emp s iff emp S ) )
assume A1:
S = Class ((==_ X),s)
; ( emp s iff emp S )
consider s1 being stack of X such that
A2:
emp s1
by Th2;
( emp S iff S in { the s_empty of X} )
by Def20;
then
( emp S iff S = the s_empty of X )
by TARSKI:def 1;
then
( emp S iff S = Class ((==_ X),s1) )
by A2, Th19;
then
( emp S iff [s,s1] in ==_ X )
by A1, EQREL_1:35;
then
( emp S iff s == s1 )
by Def16;
hence
( emp s iff emp S )
by A2, Th14, Th15; verum