let r be real number ; :: thesis: ( r > 0 implies 2 * (r / 4) < r )
assume A1: r > 0 ; :: thesis: 2 * (r / 4) < r
2 * (r / 4) = r / 2 ;
hence 2 * (r / 4) < r by A1, XREAL_1:218; :: thesis: verum