let x, y be Real; :: thesis: - [**x,y**] = [**(- x),(- y)**]
thus - [**x,y**] = - (x + (y * <i>)) by COMPLFLD:2
.= [**(- x),(- y)**] ; :: thesis: verum