:: deftheorem Def27 defines OSClass OSAFREE:def 27 :
for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X)
for b₅ being Element of OSClass (R,(LeastSort t)) holds
( b₅ = OSClass (R,t) iff for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
b₅ = OSClass (R,x) );