theorem Th16: :: OSALG_2:16

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= SubSort A