let F be ext-real-membered set ; :: thesis: for f being ExtReal holds
( f in F iff - f in -- F )
let f be ExtReal; :: thesis: ( f in F iff - f in -- F )
f in ExtREAL by XXREAL_0:def 1;
hence ( f in F implies - f in -- F ) ; :: thesis: ( - f in -- F implies f in F )
assume - f in -- F ; :: thesis: f in F
then A1: ex w being Element of ExtREAL st
( - w = - f & w in F ) ;
- (- f) = f ;
hence f in F by A1; :: thesis: verum