let X be StackAlgebra; :: thesis: for s being stack of X holds Class ((==_ X),s) is stack of (X /==)
let s be stack of X; :: thesis: Class ((==_ X),s) is stack of (X /==)
the carrier' of (X /==) = Class (==_ X) by Def20;
hence Class ((==_ X),s) is stack of (X /==) by EQREL_1:def 3; :: thesis: verum