let r, s be Real; :: thesis: ( 0 <= r & s * s < r * r implies s < r )
assume that
A1: 0 <= r and
A2: s * s < r * r ; :: thesis: s < r
assume s >= r ; :: thesis: contradiction
then ( r * s <= s * s & r * r <= s * r ) by A1, XREAL_1:64;
hence contradiction by A2, XXREAL_0:2; :: thesis: verum