let r be Real; :: thesis: - <*r*> = <*(- r)*>
reconsider s = r as Element of REAL by XREAL_0:def 1;
- <*s*> = <*(compreal . s)*> by FINSEQ_2:35
.= <*(- r)*> by BINOP_2:def 7 ;
hence - <*r*> = <*(- r)*> ; :: thesis: verum