[.0,(2 * PI).[ = [.0,PI.] \/ ].PI,(2 * PI).[ by COMPTRIG:5, XXREAL_1:169
.= ([.0,PI.[ \/ {PI}) \/ ].PI,(2 * PI).[ by COMPTRIG:5, XXREAL_1:129 ;
hence [.0,(2 * PI).[ = ([.0,PI.[ \/ {PI}) \/ ].PI,(2 * PI).[ ; :: thesis: verum