let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R
let R be ManySortedRelation of the Sorts of A; :: thesis: InvCl (StabCl R) = TRS R
A1: StabCl R c= InvCl (StabCl R) by Def11;
R c= TRS R by Def13;
then StabCl R c= TRS R by Def12;
then A2: InvCl (StabCl R) c= TRS R by Def11;
A3: InvCl (StabCl R) is invariant stable ManySortedRelation of A by Th30;
R c= StabCl R by Def12;
then R c= InvCl (StabCl R) by A1, PBOOLE:13;
then TRS R c= InvCl (StabCl R) by A3, Def13;
hence InvCl (StabCl R) = TRS R by A2, PBOOLE:146; :: thesis: verum