let P, Q be POINT of BK-model-Plane; :: thesis: ( BK_to_T2 P = BK_to_T2 Q implies P = Q )
assume A1: BK_to_T2 P = BK_to_T2 Q ; :: thesis: P = Q
( ex q being Element of BK_model st
( Q = q & BK_to_T2 Q = BK_to_REAL2 q ) & ex p being Element of BK_model st
( P = p & BK_to_T2 P = BK_to_REAL2 p ) ) by Def01;
hence P = Q by A1, BKMODEL2:4; :: thesis: verum