let P be Element of BK_model ; :: thesis: BK_to_REAL2 P in TarskiEuclid2Space
( MetrStruct(# the carrier of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the carrier of (Euclid 2), the distance of (Euclid 2) #) & BK_to_REAL2 P in TOP-REAL 2 ) by GTARSKI1:def 13;
hence BK_to_REAL2 P in TarskiEuclid2Space by EUCLID:22; :: thesis: verum