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