:: deftheorem Def1 defines OSGeneratorSet OSAFREE:def 1 :
for S being OrderSortedSign
for U0 being OSAlgebra of S
for b₃ being MSSubset of U0 holds
( b₃ is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl b₃ holds
the Sorts of (GenOSAlg O) = the Sorts of U0 );