let r1, r2, r3 be non negative Real; :: thesis: ( not r1 * r2 <= r3 or r1 <= sqrt r3 or r2 <= sqrt r3 )
assume that
A1: r1 * r2 <= r3 and
A2: ( not r1 <= sqrt r3 & not r2 <= sqrt r3 ) ; :: thesis: contradiction
sqrt r3 >= 0 by SQUARE_1:def 2;
then (sqrt r3) ^2 < r1 * r2 by A2, XREAL_1:96;
hence contradiction by A1, SQUARE_1:def 2; :: thesis: verum