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 ex mr being Real st
( - r = - mr & mr in X ) ;
hence r in X ; :: thesis: verum