reconsider p = P as Element of BK_model ;
BK_to_REAL2 p in TarskiEuclid2Space by Th01;
hence ex b₁ being POINT of TarskiEuclid2Space ex p being Element of BK_model st
( P = p & b₁ = BK_to_REAL2 p ) ; :: thesis: verum