:: deftheorem defines RVfirst FINANCE6:def 13 :
for r being Real holds RVfirst r = {1,2,3,4} --> r;