:: deftheorem defines map-reflexive ROUGHS_5:def 1 :
for R being non empty set
for I being Function of R,(bool R) holds
( I is map-reflexive iff for u being Element of R holds u in I . u );