let a be Integer; :: thesis: round a = a
a - (1 / 2) < a - 0 by XREAL_1:6;
then ( a + 0 <= a + (1 / 2) & (a + (1 / 2)) - 1 < a - 0 ) by XREAL_1:6;
hence round a = a by INT_1:def 6; :: thesis: verum