let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds
( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )
let A be non-empty MSAlgebra over S; :: thesis: for R being ManySortedRelation of A holds
( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )
let R be ManySortedRelation of A; :: thesis: ( EqCl (R,A) c= EqTh R & InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )
A1: R c= EqTh R by Def15;
hence EqCl (R,A) c= EqTh R by Th44; :: thesis: ( InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R )
thus ( InvCl R c= EqTh R & StabCl R c= EqTh R & TRS R c= EqTh R ) by A1, Def11, Def12, Def13; :: thesis: verum