let i be Integer; :: thesis: for r being Real st i <= r & r < i + 1 holds
[\r/] = i
let r be Real; :: thesis: ( i <= r & r < i + 1 implies [\r/] = i )
assume A1: i <= r ; :: thesis: ( not r < i + 1 or [\r/] = i )
assume r < i + 1 ; :: thesis: [\r/] = i
then r - 1 < (i + 1) - 1 by XREAL_1:14;
hence [\r/] = i by A1, INT_1:def 6; :: thesis: verum