let r, s be real number ; :: thesis: ( 1 < r & r * r <= s implies r < s )
assume A1: ( 1 < r & r * r <= s ) ; :: thesis: r < s
then r < r * r by XREAL_1:157;
hence r < s by A1, XXREAL_0:2; :: thesis: verum