theorem :: SQUARE_1:21

sqrt 2 < 2 by Lm3, Th20;