for P being Element of BK_model holds BK_to_REAL2 P in TarskiEuclid2Space