let x be Real; :: thesis: ( 1 < x ^2 implies (1 / x) ^2 < 1 )
assume A1: 1 < x ^2 ; :: thesis: (1 / x) ^2 < 1
then 1 / (x ^2) < (x ^2) / (x ^2) by XREAL_1:74;
then (1 ^2) / (x ^2) < 1 by A1, XCMPLX_1:60;
hence (1 / x) ^2 < 1 by XCMPLX_1:76; :: thesis: verum