:: deftheorem defines round CARDFIN2:def 1 :
for n being Real holds round n = [\(n + (1 / 2))/];