hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: INT c= CircleMap " {c[10]}
let i be object ; :: thesis: ( i in CircleMap " {c[10]} implies i in INT )
assume A1: i in CircleMap " {c[10]} ; :: thesis: i in INT
then reconsider x = i as Real ;
CircleMap . i in {c[10]} by A1, FUNCT_2:38;
then CircleMap . i = c[10] by TARSKI:def 1;
then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| = |[1,0]| by 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 object ; :: 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 ;
CircleMap . i = c[10] by Th32;
then A2: CircleMap . i in {c[10]} by TARSKI:def 1;
i in the carrier of R^1 by TOPMETR:17, XREAL_0:def 1;
hence i in CircleMap " {c[10]} by A2, FUNCT_2:38; :: thesis: verum