let P be POINT of BK-model-Plane; T2_to_BK (BK_to_T2 P) = P
consider p being Element of BK_model such that
A1:
P = p
and
A2:
BK_to_T2 P = BK_to_REAL2 p
by Def01;
consider u being non zero Element of (TOP-REAL 3) such that
A3:
Dir u = p
and
A4:
u . 3 = 1
and
A5:
BK_to_REAL2 p = |[(u . 1),(u . 2)]|
by BKMODEL2:def 2;
reconsider Q = BK_to_T2 P as POINT of TarskiEuclid2Space ;
consider v being non zero Element of (TOP-REAL 3) such that
A6:
T2_to_BK Q = Dir v
and
A7:
v `3 = 1
and
A8:
Tn2TR Q = |[(v `1),(v `2)]|
by A2, Def02;
( u . 1 = v `1 & u . 2 = v `2 )
by A8, A5, A2, FINSEQ_1:77;
then A9:
( u `1 = v `1 & u `2 = v `2 )
by EUCLID_5:def 1, EUCLID_5:def 2;
u =
|[(u `1),(u `2),(u `3)]|
by EUCLID_5:3
.=
|[(v `1),(v `2),(v `3)]|
by A4, A7, A9, EUCLID_5:def 3
.=
v
by EUCLID_5:3
;
hence
T2_to_BK (BK_to_T2 P) = P
by A1, A6, A3; verum