let x be real number ; :: 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:76;
then (1 ^2 ) / (x ^2 ) < 1 by A1, XCMPLX_1:60;
hence (1 / x) ^2 < 1 by XCMPLX_1:77; :: thesis: verum