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) = f ;
hence ( - f in F iff f in -- F ) by Th1; :: thesis: verum