let n be Nat; :: thesis: ( n >= 2 implies [/(n / 2)\] < n )
assume A1: n >= 2 ; :: thesis: [/(n / 2)\] < n

A2: now :: thesis: not (n / 2) + 1 > n

assume (n / 2) + 1 > n ; :: thesis: contradiction
then 2 * ((n / 2) + 1) > 2 * n by XREAL_1:68;
then (2 * (n / 2)) + (2 * 1) > 2 * n ;
then 2 > (2 * n) - n by XREAL_1:19;
hence contradiction by A1; :: thesis: verum

end;

[/(n / 2)\] < (n / 2) + 1 by INT_1:def 7;
hence [/(n / 2)\] < n by A2, XXREAL_0:2; :: thesis: verum