theorem :: XREAL_1:216

for a being Real st 0 < a holds
a / 2 < a by Lm27;