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