:: deftheorem Def18 defines NF-var MSAFREE4:def 18 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being ManySortedRelation of (Free (S,X)) holds
( R is NF-var iff for s being SortSymbol of S
for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s );