let P, Q be Point of BK-model-Plane; :: thesis: ( Tn2TR (BK_to_T2 P) = Tn2TR (BK_to_T2 Q) implies P = Q )
assume A1: Tn2TR (BK_to_T2 P) = Tn2TR (BK_to_T2 Q) ; :: thesis: P = Q
reconsider p = P, q = Q as Element of BK_model ;
( Tn2TR (BK_to_T2 P) = BK_to_REAL2 p & Tn2TR (BK_to_T2 Q) = BK_to_REAL2 q ) by Th04;
hence P = Q by A1, BKMODEL2:4; :: thesis: verum