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
( R c= TRS R & TRS R c= EqCl (TRS R),A ) by Def13, Th43;
then R c= EqCl (TRS R),A by PBOOLE:15;
hence EqTh R c= EqCl (TRS R),A by Def15; :: according to PBOOLE:def 13 :: 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