let P1, P2 be POINT of BK-model-Plane; :: thesis: ( 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)]| ) ; :: thesis: 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; :: thesis: verum