let X be StackAlgebra; :: thesis: 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; :: thesis: for S being stack of (X /==) st S = Class ((==_ X),s) holds
( emp s iff emp S )
let S be stack of (X /==); :: thesis: ( S = Class ((==_ X),s) implies ( emp s iff emp S ) )
assume A1: S = Class ((==_ X),s) ; :: thesis: ( emp s iff emp S )
consider s1 being stack of X such that
A2: emp s1 by Th1;
( emp S iff S in the s_empty of (X /==) ) by EMP;
then ( emp S iff S in { the s_empty of X} ) by QUOT;
then ( emp S iff S = the s_empty of X ) by TARSKI:def 1;
then ( emp S iff S = Class ((==_ X),s1) ) by A2, Th50;
then ( emp S iff [s,s1] in ==_ X ) by A1, EQREL_1:35;
then ( emp S iff s == s1 ) by REL;
hence ( emp s iff emp S ) by A2, Th42, Th43; :: thesis: verum