let r be real number ; :: thesis: for X being Subset of REAL holds
( r in X iff - r in - X )
let X be Subset of REAL ; :: thesis: ( r in X iff - r in - X )
thus ( r in X implies - r in - X ) ; :: thesis: ( - r in - X implies r in X )
assume - r in - X ; :: thesis: r in X
then consider mr being Real such that
A1: ( - r = - mr & mr in X ) ;
thus r in X by A1; :: thesis: verum