let a, b be 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 Th63
.= angle ((- a),(Rotate (b,PI))) by Th58
.= angle ((- a),(- b)) by Th58 ;
:: thesis: verum