let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra of S
for s being SortSymbol of S
for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
let U1 be MSAlgebra of S; :: thesis: for s being SortSymbol of S
for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
let s be SortSymbol of S; :: thesis: for R being MSEquivalence-like ManySortedRelation of U1 holds R . s is Equivalence_Relation of ( the Sorts of U1 . s)
let R be MSEquivalence-like ManySortedRelation of U1; :: thesis: R . s is Equivalence_Relation of ( the Sorts of U1 . s)
R is MSEquivalence_Relation-like by Def5;
hence R . s is Equivalence_Relation of ( the Sorts of U1 . s) by Def3; :: thesis: verum