theorem :: XREAL_1:215

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