:: deftheorem defines OSSubSort OSALG_2:def 8 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds OSSubSort OU0 = { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;