:: deftheorem defines nonpositive MESFUNC5:def 2 :
for R being Relation holds
( R is nonpositive iff rng R is nonpositive );