theorem :: INT_1:37

for r being Real holds [\[/r\]/] = [/r\] ;