:: deftheorem Def4 defines constant YELLOW_6:def 4 :
for S being 1-sorted
for N being NetStr over S holds
( N is constant iff the mapping of N is constant );