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 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; :: thesis: verum