:: deftheorem defines f_0 ROUGHS_5:def 6 :
for R being non empty RelStr holds f_0 R = ff_0 (tau R);