:: deftheorem Def10 defines OSSubSort OSALG_2:def 10 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being Element of S1
for b₅ being set holds
( b₅ = OSSubSort (A,s) iff for x being object holds
( x in b₅ iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) );