let m be Nat; :: thesis: ( 2 <= m implies 1 <= (2 * m) -' 2 )
assume A1: 2 <= m ; :: thesis: 1 <= (2 * m) -' 2
then 2 * 2 <= 2 * m by XREAL_1:66;
then A2: 4 - 2 <= (2 * m) - 2 by XREAL_1:9;
(2 * m) -' 2 = (2 * m) - 2 by A1, Lm7;
hence 1 <= (2 * m) -' 2 by A2, XXREAL_0:2; :: thesis: verum