MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of A, the Charact of A #) ;
then reconsider B = A as MSSubAlgebra of A by MSUALG_2:5;
take B ; :: thesis: B is feasible
thus B is feasible ; :: thesis: verum