theorem :: INT_1:40

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