:: deftheorem Def9 defines CompClass OSALG_4:def 9 :
for S being locally_directed OrderSortedSign
for A being OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of A
for C being Component of S
for b₅ being Equivalence_Relation of ( the Sorts of A -carrier_of C) holds
( b₅ = CompClass (E,C) iff for x, y being object holds
( [x,y] in b₅ iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) );