let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds R c= EqCl (R,A)
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of A holds R c= EqCl (R,A)
let R be ManySortedRelation of A; :: thesis: R c= EqCl (R,A)
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or R . i c= (EqCl (R,A)) . i )
assume i in the carrier of S ; :: thesis: R . i c= (EqCl (R,A)) . i
then reconsider s = i as SortSymbol of S ;
(EqCl (R,A)) . s = EqCl (R . s) by MSUALG_5:def 3;
hence R . i c= (EqCl (R,A)) . i by MSUALG_5:def 1; :: thesis: verum