theorem Th24: :: OSALG_2:24

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds (OSConstants OU0) (\/) A c= OSMSubSort A