for Q being Element of inside_of_circle (0,0,1) holds BK_to_REAL2 (REAL2_to_BK Q) = Q