let P1, P2 be POINT of BK-model-Plane; ( ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) & ex u being non zero Element of (TOP-REAL 3) st
( P2 = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) implies P1 = P2 )
assume that
A5:
ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| )
and
A6:
ex v being non zero Element of (TOP-REAL 3) st
( P2 = Dir v & v `3 = 1 & Tn2TR P = |[(v `1),(v `2)]| )
; P1 = P2
consider u being non zero Element of (TOP-REAL 3) such that
A7:
P1 = Dir u
and
A8:
u `3 = 1
and
A9:
Tn2TR P = |[(u `1),(u `2)]|
by A5;
consider v being non zero Element of (TOP-REAL 3) such that
A10:
P2 = Dir v
and
A11:
v `3 = 1
and
A12:
Tn2TR P = |[(v `1),(v `2)]|
by A6;
A13:
( u `1 = v `1 & u `2 = v `2 )
by A9, A12, FINSEQ_1:77;
u =
|[(v `1),(v `2),(v `3)]|
by A13, A8, A11, EUCLID_5:3
.=
v
by EUCLID_5:3
;
hence
P1 = P2
by A7, A10; verum