for s being Real st 1 < s & s + (1 / s) < sqrt 5 holds
( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 )