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
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 13 :: thesis: TRS R c= InvCl (StabCl R)
( R c= StabCl R & StabCl R c= InvCl (StabCl R) ) by Def11, Def12;
then ( InvCl (StabCl R) is invariant stable ManySortedRelation of A & R c= InvCl (StabCl R) ) by Th30, PBOOLE:15;
hence TRS R c= InvCl (StabCl R) by Def13; :: thesis: verum