let r be Real; :: thesis: ( sin r = 0 implies ex i being Integer st r = PI * i )
assume sin r = 0 ; :: thesis: ex i being Integer st r = PI * i
then ( r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) ) by Th5;
then ( r = PI * (2 * [\(r / (2 * PI))/]) or r = PI * (1 + (2 * [\(r / (2 * PI))/])) ) ;
hence ex i being Integer st r = PI * i ; :: thesis: verum