theorem Th21: :: OSALG_2:21

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)