let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A holds R c= EqCl R,A
let A be non-empty MSAlgebra of 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 set ; :: according to PBOOLE:def 5 :: 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