:: deftheorem defines f_1 ROUGHS_5:def 7 :
for R being non empty RelStr holds f_1 R = ff_0 (UncertaintyMap R);