let r, s be Real; :: thesis: ( sin r = sin s implies ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) )
assume A1: sin r = sin s ; :: thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )
A2: (sin r) - (sin s) = 2 * ((cos ((r + s) / 2)) * (sin ((r - s) / 2))) by SIN_COS4:16;

per cases ( sin ((r - s) / 2) = 0 or cos ((r + s) / 2) = 0 ) by A1, A2;

suppose sin ((r - s) / 2) = 0 ; :: thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )

hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) by Lm5; :: thesis: verum

end;

suppose cos ((r + s) / 2) = 0 ; :: thesis: ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) )

then consider i being Integer such that
A3: (r + s) / 2 = (PI / 2) + (PI * i) by Th8;
r = (PI - s) + ((2 * PI) * i) by A3;
hence ex i being Integer st
( r = s + ((2 * PI) * i) or r = (PI - s) + ((2 * PI) * i) ) ; :: thesis: verum

end;

end;