let r, s be Real; :: thesis: ( 1 < r & r * r <= s implies r < s )
assume that
A1: 1 < r and
A2: r * r <= s ; :: thesis: r < s
r < r * r by A1, XREAL_1:155;
hence r < s by A2, XXREAL_0:2; :: thesis: verum