theorem :: SQUARE_1:19

1 < sqrt 2 by Lm3, Th18;