theorem Th01: :: BKMODEL4:7

for P being Element of BK_model holds BK_to_REAL2 P in TarskiEuclid2Space