let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being ManySortedRelation of the Sorts of A holds InvCl (StabCl R) = TRS R
let A be non-empty MSAlgebra of 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;
hence InvCl (StabCl R) c= TRS R by Def11; :: according to PBOOLE:def 10 :: thesis: TRS R c= InvCl (StabCl R)
A2: 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;
hence TRS R c= InvCl (StabCl R) by A2, Def13; :: thesis: verum