:: deftheorem defines OSClass OSALG_4:def 12 :
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x being Element of the Sorts of U1 . s holds OSClass (E,x) = Class ((CompClass (E,(CComp s))),x);