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

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