let a, b be Element of COMPLEX ; :: thesis: ( a <> 0 & b <> 0 implies angle (a,b) = angle ((- a),(- b)) )
assume ( a <> 0 & b <> 0 ) ; :: thesis: angle (a,b) = angle ((- a),(- b))
hence angle (a,b) = angle ((Rotate (a,PI)),(Rotate (b,PI))) by Th79
.= angle ((- a),(Rotate (b,PI))) by Th74
.= angle ((- a),(- b)) by Th74 ;
:: thesis: verum