let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for C being MSCongruence of A st C = [|the Sorts of A,the Sorts of A|] holds
the Sorts of (QuotMSAlg A,C) = {the Sorts of A}
let A be non-empty MSAlgebra of S; :: thesis: for C being MSCongruence of A st C = [|the Sorts of A,the Sorts of A|] holds
the Sorts of (QuotMSAlg A,C) = {the Sorts of A}
let C be MSCongruence of A; :: thesis: ( C = [|the Sorts of A,the Sorts of A|] implies the Sorts of (QuotMSAlg A,C) = {the Sorts of A} )
assume A1: C = [|the Sorts of A,the Sorts of A|] ; :: thesis: the Sorts of (QuotMSAlg A,C) = {the Sorts of A}

now

let i be set ; :: thesis: ( i in the carrier of S implies the Sorts of (QuotMSAlg A,C) . i = {the Sorts of A} . i )
assume i in the carrier of S ; :: thesis: the Sorts of (QuotMSAlg A,C) . i = {the Sorts of A} . i
then reconsider s = i as Element of S ;
A2: C . s = [:(the Sorts of A . s),(the Sorts of A . s):] by A1, PBOOLE:def 21
.= nabla (the Sorts of A . s) by EQREL_1:def 1 ;
thus the Sorts of (QuotMSAlg A,C) . i = Class (C . s) by MSUALG_4:def 8
.= {(the Sorts of A . s)} by A2, Th5
.= {the Sorts of A} . i by PZFMISC1:def 1 ; :: thesis: verum

end;

hence the Sorts of (QuotMSAlg A,C) = {the Sorts of A} by PBOOLE:3; :: thesis: verum