theorem Th27: :: MSAFREE4:27

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
B2 is opers_closed by Th24;