let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over 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 over 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 object ; :: according to PBOOLE:def 2 :: 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 ;
A2: (EqCl (R,A)) . s = EqCl (R . s) by MSUALG_5:def 3;
R . s c= E . s by A1;
hence (EqCl (R,A)) . i c= E . i by A2, MSUALG_5:def 1; :: thesis: verum