theorem Th25: :: INT_1:25

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