let P be Point of BK-model-Plane; :: thesis: for p being Element of BK_model st P = p holds
( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p )
let p be Element of BK_model ; :: thesis: ( P = p implies ( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p ) )
assume A1: P = p ; :: thesis: ( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p )
ex p being Element of BK_model st
( P = p & BK_to_T2 P = BK_to_REAL2 p ) by Def01;
hence ( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p ) by A1; :: thesis: verum