let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for R being stable ManySortedRelation of A holds StabCl R = R
let A be non-empty MSAlgebra of S; :: thesis: for R being stable ManySortedRelation of A holds StabCl R = R
let R be stable ManySortedRelation of A; :: thesis: StabCl R = R
thus ( StabCl R c= R & R c= StabCl R ) by Def12; :: according to PBOOLE:def 10 :: thesis: verum