reconsider o = 0 as Element of REAL by Lm3;
let x, y be Element of REAL ; :: thesis: opp (+ (x,y)) = + ((opp x),(opp y))
+ ((+ (x,y)),(+ ((opp x),(opp y)))) = + (x,(+ (y,(+ ((opp x),(opp y)))))) by Th23
.= + (x,(+ ((opp x),(+ (y,(opp y)))))) by Th23
.= + (x,(+ ((opp x),o))) by Def3
.= + (x,(opp x)) by Th11
.= 0 by Def3 ;
hence opp (+ (x,y)) = + ((opp x),(opp y)) by Def3; :: thesis: verum