A1: ((sin (PI / 3)) ^2) + ((cos (PI / 3)) ^2) = 1 by SIN_COS:29;
A2: (cos (PI / 3)) ^2 = (cos (PI / 3)) * (cos (PI / 3)) by SQUARE_1:def 1
.= 1 / 4 by Thm8 ;
sin (PI / 3) >= 0

proof

A3: (PI / 2) - (PI / 3) in ].0,(PI / 2).[

proof

set n = (PI / 2) - (PI / 3);
PI / 6 < PI / 2 by COMPTRIG:5, XREAL_1:76;
hence (PI / 2) - (PI / 3) in ].0,(PI / 2).[ by COMPTRIG:5, XXREAL_1:4; :: thesis: verum

end;

sin (PI / 3) = cos ((PI / 2) - (PI / 3)) by SIN_COS:79;
hence sin (PI / 3) >= 0 by A3, SIN_COS:81; :: thesis: verum

end;

then sin (PI / 3) = sqrt (3 / 4) by A1, A2, SQUARE_1:22;
hence sin (PI / 3) = (sqrt 3) / 2 by SQUARE_1:20, SQUARE_1:30; :: thesis: verum