theorem :: XREAL_1:221

for a being Real st 0 < a holds
a / 3 < a