reconsider p = Tn2TR P as Element of inside_of_circle (0,0,1) by A1;
reconsider Q = REAL2_to_BK p as Element of BK_model ;
consider P2 being Element of (TOP-REAL 2) such that
A2: P2 = p and
A3: REAL2_to_BK p = Dir |[(P2 `1),(P2 `2),1]| by BKMODEL2:def 3;
reconsider u = |[(P2 `1),(P2 `2),1]| as non zero Element of (TOP-REAL 3) ;
now :: thesis: ( Q = Dir u & u `3 = 1 & p = |[(u `1),(u `2)]| )
thus Q = Dir u by A3; :: thesis: ( u `3 = 1 & p = |[(u `1),(u `2)]| )
|[(u `1),(u `2),(u `3)]| = |[(P2 `1),(P2 `2),1]| by EUCLID_5:3;
then A4: ( u `1 = P2 `1 & u `2 = P2 `2 & u `3 = 1 ) by FINSEQ_1:78;
thus u `3 = 1 by EUCLID_5:2; :: thesis: p = |[(u `1),(u `2)]|
thus p = |[(u `1),(u `2)]| by A2, A4, EUCLID:53; :: thesis: verum
end;
hence ex b1 being POINT of BK-model-Plane ex u being non zero Element of (TOP-REAL 3) st
( b1 = Dir u & u `3 = 1 & Tn2TR P = |[(u `1),(u `2)]| ) ; :: thesis: verum