theorem Th30: :: INT_1:30

for r being Real holds
( [/r\] = r iff r is integer )