:: deftheorem CONTEXT defines -context MSAFREE5:def 20 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s
for r being Element of T holds
( r is x -context iff card (Coim (r,[x,s])) = 1 );