let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra over 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 over 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 Def3;
hence R . s is Equivalence_Relation of ( the Sorts of U1 . s) by Def2; :: thesis: verum