theorem :: XREAL_1:222

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