theorem Th17: :: MSSUBLAT:17
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)