:: deftheorem Def14 defines OSSub OSALG_2:def 14 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for b₃ being set holds
( b₃ = OSSub OU0 iff for x being object holds
( x in b₃ iff x is strict OSSubAlgebra of OU0 ) );