let a be Real; :: thesis: [/a\] <= [\a/] + 1

per cases ( a is integer or not a is integer ) ;

suppose a is integer ; :: thesis: [/a\] <= [\a/] + 1

then reconsider a = a as Integer ;
[/a\] <= a + 1 by INT_1:def 7;
hence [/a\] <= [\a/] + 1 ; :: thesis: verum

end;

suppose not a is integer ; :: thesis: [/a\] <= [\a/] + 1

hence [/a\] <= [\a/] + 1 by INT_1:34, INT_1:41; :: thesis: verum

end;

end;