let X be StackAlgebra; :: thesis: for S being stack of (X /==) ex s being stack of X st S = Class ((==_ X),s)
let S be stack of (X /==); :: thesis: ex s being stack of X st S = Class ((==_ X),s)
the carrier' of (X /==) = Class (==_ X) by Def20;
then S in Class (==_ X) ;
then ex x being object st
( x in the carrier' of X & S = Class ((==_ X),x) ) by EQREL_1:def 3;
hence ex s being stack of X st S = Class ((==_ X),s) ; :: thesis: verum