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