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