Constructive?

剛開始看主教與橋的《Constructive Analysis》，在 p.19 有一個論證步驟是

其中 x_n 和 y_n 是有理數。這一句應該是從下面這個命題證得：

要證明這個命題，應該是論述「如果 a > 0，則…」，這個論述在形式上是

但這在 intuitionistic logic 裡面並非 tautology！還是說那個命題有別種證法，或是說 Bishop and Bridges 採用的是某種比較寬鬆的 constructive logic？

--
在基礎上就遇到問題 XD。