:: deftheorem Def10 defines OSClass OSALG_4:def 10 :
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for s1 being Element of S
for b₅ being Subset of (Class (CompClass (E,(CComp s1)))) holds
( b₅ = OSClass (E,s1) iff for z being set holds
( z in b₅ iff ex x being set st
( x in the Sorts of A . s1 & z = Class ((CompClass (E,(CComp s1))),x) ) ) );