let P, Q be Element of BK_model ; ( P = Q iff BK_to_REAL2 P = BK_to_REAL2 Q )
thus
( P = Q implies BK_to_REAL2 P = BK_to_REAL2 Q )
; ( BK_to_REAL2 P = BK_to_REAL2 Q implies P = Q )
assume A1:
BK_to_REAL2 P = BK_to_REAL2 Q
; P = Q
consider u being non zero Element of (TOP-REAL 3) such that
A2:
( Dir u = P & u . 3 = 1 & BK_to_REAL2 P = |[(u . 1),(u . 2)]| )
by Def01;
consider v being non zero Element of (TOP-REAL 3) such that
A3:
( Dir v = Q & v . 3 = 1 & BK_to_REAL2 Q = |[(v . 1),(v . 2)]| )
by Def01;
( u . 1 = v . 1 & u . 2 = v . 2 & u . 3 = v . 3 )
by A1, A2, A3, FINSEQ_1:77;
then
( u `1 = v . 1 & u `2 = v . 2 & u `3 = v . 3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then A4:
( u `1 = v `1 & u `2 = v `2 & u `3 = v `3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
( u = |[(u `1),(u `2),(u `3)]| & v = |[(v `1),(v `2),(v `3)]| )
by EUCLID_5:3;
hence
P = Q
by A2, A3, A4; verum