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
( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of the Sorts of A holds
( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )
let R be ManySortedRelation of the Sorts of A; :: thesis: ( StabCl R c= TRS R & InvCl R c= TRS R & StabCl (InvCl R) c= TRS R )
R c= TRS R by Def13;
hence ( StabCl R c= TRS R & InvCl R c= TRS R ) by Def11, Def12; :: thesis: StabCl (InvCl R) c= TRS R
hence StabCl (InvCl R) c= TRS R by Def12; :: thesis: verum