|[(- 1),(- Q),(- Q)]| = - c100 by EUCLID_5:11
.= - c[100] ;
hence |[(- 1),0,0]| is Point of (Tunit_circle 3) by TOPREALC:60; :: thesis: verum