theorem Th18: :: OSALG_2:18

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