theorem :: MEASURE6:40
for r being Real
for X being Subset of REAL holds
( r in X iff - r in -- X ) by MEMBER_1:11;