let r, s be real number ; :: thesis: ( 0 <= r & s * s < r * r implies s < r )
assume A1: ( 0 <= r & s * s < r * r ) ; :: thesis: s < r
assume A2: s >= r ; :: thesis: contradiction
then A3: r * s <= s * s by A1, XREAL_1:66;
r * r <= s * r by A1, A2, XREAL_1:66;
hence contradiction by A1, A3, XXREAL_0:2; :: thesis: verum