theorem :: XREAL_1:224

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