let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)
let A be non-empty MSAlgebra of S; :: thesis: for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)
let R be ManySortedRelation of A; :: thesis: EqTh R = EqCl ((TRS R),A)
A1: TRS R c= EqCl ((TRS R),A) by Th43;
R c= TRS R by Def13;
then R c= EqCl ((TRS R),A) by A1, PBOOLE:13;
hence EqTh R c= EqCl ((TRS R),A) by Def15; :: according to PBOOLE:def 10 :: thesis: EqCl ((TRS R),A) c= EqTh R
R c= EqTh R by Def15;
then TRS R c= EqTh R by Def13;
hence EqCl ((TRS R),A) c= EqTh R by Th44; :: thesis: verum