let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)
let A be non-empty MSAlgebra over 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;
then A2: EqTh R c= EqCl ((TRS R),A) by Def15;
R c= EqTh R by Def15;
then TRS R c= EqTh R by Def13;
then EqCl ((TRS R),A) c= EqTh R by Th44;
hence EqTh R = EqCl ((TRS R),A) by A2, PBOOLE:146; :: thesis: verum