:: deftheorem Def12 defines GenOSAlg OSALG_2:def 12 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for b₄ being strict OSSubAlgebra of OU0 holds
( b₄ = GenOSAlg A iff ( A is OSSubset of b₄ & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b₄ is OSSubAlgebra of OU1 ) ) );