:: deftheorem Def5 defines SubAlgCl CLOSURE3:def 5 :
for S being non empty non void ManySortedSign
for MA being non-empty MSAlgebra over S
for b₃ being strict ClosureStr over 1-sorted(# the carrier of S #) holds
( b₃ = SubAlgCl MA iff ( the Sorts of b₃ = the Sorts of MA & the Family of b₃ = SubSort MA ) );