:: deftheorem Def17 defines with_UN_property MSAFREE4:def 17 :
for I being set
for X being ManySortedSet of I
for R being ManySortedRelation of X holds
( R is with_UN_property iff for x being set st x in I holds
R . x is with_UN_property );