theorem Th22: :: OSALG_2:22

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)