let S be non empty non void ManySortedSign ; 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; for R being ManySortedRelation of A holds EqTh R = EqCl ((TRS R),A)
let R be ManySortedRelation of A; 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; verum