let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A
for E being MSEquivalence-like ManySortedRelation of A st R c= E holds
EqCl R,A c= E
let A be non-empty MSAlgebra of S; :: thesis: for R being ManySortedRelation of A
for E being MSEquivalence-like ManySortedRelation of A st R c= E holds
EqCl R,A c= E
let R be ManySortedRelation of A; :: thesis: for E being MSEquivalence-like ManySortedRelation of A st R c= E holds
EqCl R,A c= E
let E be MSEquivalence-like ManySortedRelation of A; :: thesis: ( R c= E implies EqCl R,A c= E )
assume A1: R c= E ; :: thesis: EqCl R,A c= E
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or (EqCl R,A) . i c= E . i )
assume i in the carrier of S ; :: thesis: (EqCl R,A) . i c= E . i
then reconsider s = i as SortSymbol of S ;
( (EqCl R,A) . s = EqCl (R . s) & R . s c= E . s & E . s is Equivalence_Relation of the Sorts of A . s ) by A1, MSUALG_5:def 3, PBOOLE:def 5;
hence (EqCl R,A) . i c= E . i by MSUALG_5:def 1; :: thesis: verum