let r be Real; :: thesis: for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )
let X be Subset of REAL; :: thesis: ( r in X iff 1 / r in Inv X )
thus ( r in X implies 1 / r in Inv X ) ; :: thesis: ( 1 / r in Inv X implies r in X )
assume 1 / r in Inv X ; :: thesis: r in X
then ex mr being Real st
( 1 / r = 1 / mr & mr in X ) ;
hence r in X by XCMPLX_1:59; :: thesis: verum