hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: INT c= CircleMap " {c[10] }

let i be set ; :: thesis: ( i in CircleMap " {c[10] } implies i in INT )
assume A1: i in CircleMap " {c[10] } ; :: thesis: i in INT
then CircleMap . i in {c[10] } by FUNCT_2:46;
then A2: CircleMap . i = c[10] by TARSKI:def 1;
reconsider x = i as Real by A1, TOPMETR:24;
|[(cos ((2 * PI ) * x)),(sin ((2 * PI ) * x))]| = |[1,0 ]| by A2, Def11;
then cos ((2 * PI ) * x) = 1 by SPPOL_2:1;
hence i in INT by SIN_COS6:44; :: thesis: verum

end;

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in INT or i in CircleMap " {c[10] } )
assume i in INT ; :: thesis: i in CircleMap " {c[10] }
then reconsider i = i as Integer ;
A3: i in the carrier of R^1 by TOPMETR:24, XREAL_0:def 1;
CircleMap . i = c[10] by Th33;
then CircleMap . i in {c[10] } by TARSKI:def 1;
hence i in CircleMap " {c[10] } by A3, FUNCT_2:46; :: thesis: verum