:: deftheorem Def11 defines OSClass OSALG_4:def 11 :
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for b₄ being OrderSortedSet of S holds
( b₄ = OSClass E iff for s1 being Element of S holds b₄ . s1 = OSClass (E,s1) );