let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S holds A tolerates A
let A be MSAlgebra of S; :: thesis: A tolerates A
thus S tolerates S ; :: according to CIRCCOMB:def 3 :: thesis: ( the Sorts of A tolerates the Sorts of A & the Charact of A tolerates the Charact of A )
thus ( the Sorts of A tolerates the Sorts of A & the Charact of A tolerates the Charact of A ) ; :: thesis: verum